Module

Place_taylorCoeff_add.lean

Nyll.AlgebraicCurves.Places.Place_taylorCoeff_add

3 declarations indexed from sourceView source ↗

Module documentation

Place taylor Coeff add

Imports4

Imported by6

theorem

evalAt_add_of_mem

L32 ↗

AlgebraicCurves.Places.Proofs.Place_taylorCoeff_add.ProofAuxJetT4.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_add
open AlgebraicCurve AlgebraicCurve.Place
namespace ProofAuxJetT4
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

evalAt_smul_of_mem

L40 ↗

AlgebraicCurves.Places.Proofs.Place_taylorCoeff_add.ProofAuxJetT4.evalAt_smul_of_mem

Source context 6 commands

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

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

Lean source · statement

theorem evalAt_smul_of_mem (v : Place K F) (hv : v.IsRational) (c : K) {f : F}
    (hf : f ∈ v.toValuationSubring) : v.evalAt (c • f) = c * v.evalAt f

theorem

taylorCoeff_add

L47 ↗

AlgebraicCurve.Place.taylorCoeff_add

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_taylorCoeff_add
open AlgebraicCurve AlgebraicCurve.Place
open ProofAuxJetT4 in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.taylorCoeff_add
    {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) = taylorCoeff v t r f + taylorCoeff v t r g

Module documentation

Place taylor Coeff add

Declarations

evalAt_add_of_mem

evalAt_smul_of_mem

taylorCoeff_add