Module

Place_taylorCoeff_mul.lean

Nyll.AlgebraicCurves.Places.Place_taylorCoeff_mul

6 declarations indexed from sourceView source ↗

Module documentation

Place taylor Coeff mul

Imports7

Imported by5

theorem

evalAt_add_of_mem

L35 ↗

AlgebraicCurves.Places.Proofs.Place_taylorCoeff_mul.ProofAuxJetT6.evalAt_add_of_mem

Source context 6 commands

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

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

Lean source · statement

theorem evalAt_add_of_mem (v : Place K F) (hv : v.IsRational) {f g : F}
    (hf : f ∈ v.toValuationSubring) (hg : g ∈ v.toValuationSubring) :
    v.evalAt (f + g) = v.evalAt f + v.evalAt g

theorem

ord_nonneg_of_mem

L43 ↗

AlgebraicCurves.Places.Proofs.Place_taylorCoeff_mul.ProofAuxJetT6.ord_nonneg_of_mem

Source context 6 commands

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

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

Lean source · statement

theorem ord_nonneg_of_mem (v : Place K F) {f : F} (hf : f ∈ v.toValuationSubring) (hf0 : f ≠ 0) :
    0 ≤ v.ord f

theorem

mem_of_ord_eq_one

L47 ↗

AlgebraicCurves.Places.Proofs.Place_taylorCoeff_mul.ProofAuxJetT6.mem_of_ord_eq_one

Source context 6 commands

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

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

Lean source · statement

theorem mem_of_ord_eq_one (v : Place K F) {t : F} (ht : v.ord t = 1) : t ∈ v.toValuationSubring

theorem

evalAt_mul_eq_zero_of_ord_eq_one

L52 ↗

AlgebraicCurves.Places.Proofs.Place_taylorCoeff_mul.ProofAuxJetT6.evalAt_mul_eq_zero_of_ord_eq_one

Source context 6 commands

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

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

Lean source · statement

theorem evalAt_mul_eq_zero_of_ord_eq_one (v : Place K F) {t h : F}
    (ht : v.ord t = 1) (hh : h ∈ v.toValuationSubring) : v.evalAt (t * h) = 0

theorem

taylorRem_one

L71 ↗

AlgebraicCurves.Places.Proofs.Place_taylorCoeff_mul.ProofAuxJetT6.taylorRem_one

Source context 6 commands

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

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

Lean source · statement

theorem taylorRem_one (v : Place K F) (t f : F) :
    taylorRem v t f 1 = (f - algebraMap K F (v.evalAt f)) * t⁻¹

theorem

taylorCoeff_mul

L77 ↗

AlgebraicCurve.Place.taylorCoeff_mul

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_taylorCoeff_mul
open AlgebraicCurve AlgebraicCurve.Place
open ProofAuxJetT6 in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.taylorCoeff_mul
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : Place K F) (hv : v.IsRational) {t : F} (ht : v.ord t = 1) {f g : F}
    (hf : f ∈ v.toValuationSubring) (hg : g ∈ v.toValuationSubring) (r : ℕ) :
    taylorCoeff v t r (f * g)
      = ∑ x ∈ Finset.HasAntidiagonal.antidiagonal r, taylorCoeff v t x.1 f * taylorCoeff v t x.2 g

Module documentation

Place taylor Coeff mul

Declarations

evalAt_add_of_mem

ord_nonneg_of_mem

mem_of_ord_eq_one

evalAt_mul_eq_zero_of_ord_eq_one

taylorRem_one

taylorCoeff_mul