Module

Place_taylorRem_smul.lean

Nyll.AlgebraicCurves.Places.Place_taylorRem_smul

3 declarations indexed from sourceView source ↗

Module documentation

Place taylor Rem smul

Imports3

Imported by2

theorem

evalAt_add_of_mem

L31 ↗

AlgebraicCurves.Places.Proofs.Place_taylorRem_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_taylorRem_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

L39 ↗

AlgebraicCurves.Places.Proofs.Place_taylorRem_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_taylorRem_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

taylorRem_smul

L46 ↗

AlgebraicCurve.Place.taylorRem_smul

Source context 4 commands

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

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

Lean source · statement

theorem _root_.AlgebraicCurve.Place.taylorRem_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 : ℕ) :
    taylorRem v t (c • f) r = c • taylorRem v t f r

Module documentation

Place taylor Rem smul

Declarations

evalAt_add_of_mem

evalAt_smul_of_mem

taylorRem_smul