Module

Place_ord_norm_sub_eq_ord_eval.lean

Nyll.AlgebraicCurves.Places.Place_ord_norm_sub_eq_ord_eval

3 declarations indexed from sourceView source ↗

Module documentation

Place ord norm sub eq ord eval

Imports2

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

Imported by2

theorem

norm_algebraMap_sub

L32 ↗

AlgebraicCurves.Places.Proofs.Place_ord_norm_sub_eq_ord_eval.S09NR.norm_algebraMap_sub

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_norm_sub_eq_ord_eval
open Polynomial IntermediateField AlgebraicCurve
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.Places.Proofs.Place_ord_norm_sub_eq_ord_eval.S09NR.ord_norm_sub_eq

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_norm_sub_eq_ord_eval
open Polynomial IntermediateField AlgebraicCurve
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

ord_norm_sub_eq_ord_eval

L90 ↗

AlgebraicCurve.Place.ord_norm_sub_eq_ord_eval

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_ord_norm_sub_eq_ord_eval
open Polynomial IntermediateField AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.Place.ord_norm_sub_eq_ord_eval {K F F' : Type*} [Field K] [Field F]
  [Field F'] [Algebra K F] [Algebra F F'] [Module.Finite F F'] (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)

Module documentation

Place ord norm sub eq ord eval

Declarations

norm_algebraMap_sub

ord_norm_sub_eq

ord_norm_sub_eq_ord_eval