Module

Algebra_norm_algebraMap_sub_eq_minpoly_eval.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_norm_algebraMap_sub_eq_minpoly_eval

3 declarations indexed from sourceView source ↗

Module documentation

Algebra norm algebra Map sub eq minpoly eval

Imports2

Mathlib.RingTheory.Norm.Transitivity
Nyll.AlgebraicCurves.Places.OverDVR

Imported by2

theorem

norm_algebraMap_sub

L32 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_norm_algebraMap_sub_eq_minpoly_eval.S09NR.norm_algebraMap_sub

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_norm_algebraMap_sub_eq_minpoly_eval
open Polynomial IntermediateField
namespace S09NR
section Norm
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F'] [Module.Finite F F']

Lean source · statement

theorem norm_algebraMap_sub (x : F') (hdeg : (minpoly F x).natDegree = Module.finrank F F') (c : F)
  :
    Algebra.norm F (algebraMap F F' c - x) = (minpoly F x).eval c

theorem

ord_norm_sub_eq

L68 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_norm_algebraMap_sub_eq_minpoly_eval.S09NR.ord_norm_sub_eq

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_norm_algebraMap_sub_eq_minpoly_eval
open Polynomial IntermediateField
namespace S09NR
section Ord
open AlgebraicCurve
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra F F']
  [Module.Finite F F']

Lean source · statement

theorem ord_norm_sub_eq (v : Place K F) (Q : Polynomial v.toValuationSubring) {x : F'}
    (hQ : Q.map (algebraMap v.toValuationSubring F) = minpoly F x)
    (hdeg : (minpoly F x).natDegree = Module.finrank F F') (b : v.toValuationSubring) :
    v.ord (Algebra.norm F (x - algebraMap F F' (b : F))) = v.ord ((Q.eval b : v.toValuationSubring)
      : F)

theorem

norm_algebraMap_sub_eq_minpoly_eval

L90 ↗

Algebra.norm_algebraMap_sub_eq_minpoly_eval

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_norm_algebraMap_sub_eq_minpoly_eval
open Polynomial IntermediateField

Lean source · statement

theorem _root_.Algebra.norm_algebraMap_sub_eq_minpoly_eval {F F' : Type*} [Field F] [Field F']
  [Algebra F F'] [Module.Finite F F'] (x : F') (hdeg : (minpoly F x).natDegree = Module.finrank F
  F') (c : F) : Algebra.norm F (algebraMap F F' c - x) = (minpoly F x).eval c

Module documentation

Algebra norm algebra Map sub eq minpoly eval

Declarations

norm_algebraMap_sub

ord_norm_sub_eq

norm_algebraMap_sub_eq_minpoly_eval