Module

Place_evalEval_C_add_X_mk_taylorCoeff_eq_zero.lean

Nyll.AlgebraicCurves.Places.Place_evalEval_C_add_X_mk_taylorCoeff_eq_zero

5 declarations indexed from sourceView source ↗

Module documentation

Place eval Eval C add X mk taylor Coeff eq zero

Imports5

Imported by4

theorem

taylorRem_zero_fun

L33 ↗

AlgebraicCurves.Places.Proofs.Place_evalEval_C_add_X_mk_taylorCoeff_eq_zero.ProofAuxG2.taylorRem_zero_fun

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalEval_C_add_X_mk_taylorCoeff_eq_zero
open AlgebraicCurve AlgebraicCurve.Place Polynomial
namespace ProofAuxG2
open AlgebraicCurve AlgebraicCurve.Place Polynomial
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem taylorRem_zero_fun (v : Place K F) (t : F) (r : ℕ) : taylorRem v t 0 r = 0

theorem

taylorCoeff_zero_fun

L40 ↗

AlgebraicCurves.Places.Proofs.Place_evalEval_C_add_X_mk_taylorCoeff_eq_zero.ProofAuxG2.taylorCoeff_zero_fun

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalEval_C_add_X_mk_taylorCoeff_eq_zero
open AlgebraicCurve AlgebraicCurve.Place Polynomial
namespace ProofAuxG2
open AlgebraicCurve AlgebraicCurve.Place Polynomial
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem taylorCoeff_zero_fun (v : Place K F) (t : F) (r : ℕ) : taylorCoeff v t r 0 = 0

theorem

taylorRem_algebraMap_one

L43 ↗

AlgebraicCurves.Places.Proofs.Place_evalEval_C_add_X_mk_taylorCoeff_eq_zero.ProofAuxG2.taylorRem_algebraMap_one

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalEval_C_add_X_mk_taylorCoeff_eq_zero
open AlgebraicCurve AlgebraicCurve.Place Polynomial
namespace ProofAuxG2
open AlgebraicCurve AlgebraicCurve.Place Polynomial
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem taylorRem_algebraMap_one (v : Place K F) (t : F) (c : K) :
    taylorRem v t (algebraMap K F c) 1 = 0

theorem

evalAt_eq_zero_of_ord_pos

L48 ↗

AlgebraicCurves.Places.Proofs.Place_evalEval_C_add_X_mk_taylorCoeff_eq_zero.ProofAuxG2.evalAt_eq_zero_of_ord_pos

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalEval_C_add_X_mk_taylorCoeff_eq_zero
open AlgebraicCurve AlgebraicCurve.Place Polynomial
namespace ProofAuxG2
open AlgebraicCurve AlgebraicCurve.Place Polynomial
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem evalAt_eq_zero_of_ord_pos (v : Place K F) {g : F} (hg0 : g ≠ 0) (hpos : 0 < v.ord g) :
    v.evalAt g = 0

theorem

evalEval_C_add_X_mk_taylorCoeff_eq_zero

L64 ↗

AlgebraicCurve.Place.evalEval_C_add_X_mk_taylorCoeff_eq_zero

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalEval_C_add_X_mk_taylorCoeff_eq_zero
open AlgebraicCurve AlgebraicCurve.Place Polynomial
open ProofAuxG2 in

Lean source · full declaration

theorem _root_.AlgebraicCurve.Place.evalEval_C_add_X_mk_taylorCoeff_eq_zero
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : Place K F) (hv : v.IsRational) {z y : F}
    (hz : z ∈ v.toValuationSubring) (hy : y ∈ v.toValuationSubring)
    (ht : v.ord (z - algebraMap K F (v.evalAt z)) = 1)
    (G : Polynomial (Polynomial K))
    (hG : (G.map (Polynomial.mapRingHom (algebraMap K F))).evalEval z y = 0) :
    (G.map (Polynomial.mapRingHom (algebraMap K (PowerSeries K)))).evalEval
        (PowerSeries.C (v.evalAt z) + PowerSeries.X)
        (PowerSeries.mk fun n => taylorCoeff v (z - algebraMap K F (v.evalAt z)) n y) = 0 := by
  have h := mk_taylorCoeff_evalEval v hv ht hz hy G
  rw [hG, mk_taylorCoeff_eq_C_add_X v hv hz ht] at h
  rw [← h]
  ext n
  rw [PowerSeries.coeff_mk, taylorCoeff_zero_fun, map_zero]

Module documentation

Place eval Eval C add X mk taylor Coeff eq zero

Declarations

taylorRem_zero_fun

taylorCoeff_zero_fun

taylorRem_algebraMap_one

evalAt_eq_zero_of_ord_pos

evalEval_C_add_X_mk_taylorCoeff_eq_zero