Module

Place_mk_taylorCoeff_eq_C_add_X.lean

Nyll.AlgebraicCurves.Places.Place_mk_taylorCoeff_eq_C_add_X

5 declarations indexed from sourceView source ↗

Module documentation

Place mk taylor Coeff eq C add X

Imports6

Imported by4

theorem

taylorRem_zero_fun

L34 ↗

AlgebraicCurves.Places.Proofs.Place_mk_taylorCoeff_eq_C_add_X.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_mk_taylorCoeff_eq_C_add_X
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

L41 ↗

AlgebraicCurves.Places.Proofs.Place_mk_taylorCoeff_eq_C_add_X.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_mk_taylorCoeff_eq_C_add_X
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

L44 ↗

AlgebraicCurves.Places.Proofs.Place_mk_taylorCoeff_eq_C_add_X.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_mk_taylorCoeff_eq_C_add_X
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

L49 ↗

AlgebraicCurves.Places.Proofs.Place_mk_taylorCoeff_eq_C_add_X.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_mk_taylorCoeff_eq_C_add_X
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

mk_taylorCoeff_eq_C_add_X

L65 ↗

AlgebraicCurve.Place.mk_taylorCoeff_eq_C_add_X

Source context 4 commands

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

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

Lean source · full declaration

theorem _root_.AlgebraicCurve.Place.mk_taylorCoeff_eq_C_add_X
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : Place K F) (_hv : v.IsRational) {z : F} (_hz : z ∈ v.toValuationSubring)
    (ht : v.ord (z - algebraMap K F (v.evalAt z)) = 1) :
    (PowerSeries.mk fun n => taylorCoeff v (z - algebraMap K F (v.evalAt z)) n z)
      = PowerSeries.C (v.evalAt z) + PowerSeries.X := by
  set t : F := z - algebraMap K F (v.evalAt z) with htdef
  have ht0 : t ≠ 0 := by rintro h; rw [h] at ht; simp [Place.ord_zero] at ht
  have h1 : taylorRem v t z 1 = 1 := by
    change (taylorRem v t z 0 - _) * t⁻¹ = 1
    rw [taylorRem_zero, ← htdef, mul_inv_cancel₀ ht0]
  ext n
  rw [PowerSeries.coeff_mk, map_add, PowerSeries.coeff_C, PowerSeries.coeff_X]
  rcases n with _ | n
  · simp [taylorCoeff_zero]
  · rw [taylorCoeff_succ_eq_taylorCoeff_taylorRem_one, h1, ← map_one (algebraMap K F),
      taylorCoeff_algebraMap]
    rcases n with _ | n
    · simp
    · rw [ite_eq_right (Nat.succ_ne_zero _), ite_eq_right (Nat.succ_ne_zero _),
        ite_eq_right (by omega), add_zero]

Module documentation

Place mk taylor Coeff eq C add X

Declarations

taylorRem_zero_fun

taylorCoeff_zero_fun

taylorRem_algebraMap_one

evalAt_eq_zero_of_ord_pos

mk_taylorCoeff_eq_C_add_X