Module

Place_taylorCoeff_smul.lean

Nyll.AlgebraicCurves.Places.Place_taylorCoeff_smul

3 declarations indexed from sourceView source ↗

Module documentation

Place taylor Coeff smul

Imports4

Imported by3

theorem

evalAt_add_of_mem

L32 ↗

AlgebraicCurves.Places.Proofs.Place_taylorCoeff_smul.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_smul
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_smul.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_smul
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_smul

L47 ↗

AlgebraicCurve.Place.taylorCoeff_smul

Source context 4 commands

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

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

Lean source · statement

theorem _root_.AlgebraicCurve.Place.taylorCoeff_smul
    {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 : F}
    (hf : f ∈ v.toValuationSubring) (c : K) (r : ℕ) :
    taylorCoeff v t r (c • f) = c * taylorCoeff v t r f

Module documentation

Place taylor Coeff smul

Declarations

evalAt_add_of_mem

evalAt_smul_of_mem

taylorCoeff_smul