Module

Place_taylorCoeff_algebraMap.lean

Nyll.AlgebraicCurves.Places.Place_taylorCoeff_algebraMap

5 declarations indexed from sourceView source ↗

Module documentation

Place taylor Coeff algebra Map

Imports4

Imported by5

theorem

taylorRem_zero_fun

L32 ↗

AlgebraicCurves.Places.Proofs.Place_taylorCoeff_algebraMap.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_taylorCoeff_algebraMap
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

L39 ↗

AlgebraicCurves.Places.Proofs.Place_taylorCoeff_algebraMap.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_taylorCoeff_algebraMap
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

L42 ↗

AlgebraicCurves.Places.Proofs.Place_taylorCoeff_algebraMap.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_taylorCoeff_algebraMap
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

L47 ↗

AlgebraicCurves.Places.Proofs.Place_taylorCoeff_algebraMap.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_taylorCoeff_algebraMap
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

taylorCoeff_algebraMap

L63 ↗

AlgebraicCurve.Place.taylorCoeff_algebraMap

Source context 4 commands

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

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

Lean source · full declaration

theorem _root_.AlgebraicCurve.Place.taylorCoeff_algebraMap
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : Place K F) (t : F) (c : K) (n : ℕ) :
    taylorCoeff v t n (algebraMap K F c) = if n = 0 then c else 0 := by
  rcases n with _ | n
  · rw [ite_eq_left rfl, taylorCoeff_zero, v.evalAt_algebraMap_eq]
  · rw [ite_eq_right (Nat.succ_ne_zero n), taylorCoeff_succ_eq_taylorCoeff_taylorRem_one,
      taylorRem_algebraMap_one, taylorCoeff_zero_fun]

Module documentation

Place taylor Coeff algebra Map

Declarations

taylorRem_zero_fun

taylorCoeff_zero_fun

taylorRem_algebraMap_one

evalAt_eq_zero_of_ord_pos

taylorCoeff_algebraMap