Module

Place_taylorRem_mem_toValuationSubring.lean

Nyll.AlgebraicCurves.Places.Place_taylorRem_mem_toValuationSubring

4 declarations indexed from sourceView source ↗

Module documentation

Place taylor Rem mem to Valuation Subring

Imports3

Imported by6

theorem

evalAt_sub_of_mem'

L31 ↗

AlgebraicCurves.Places.Proofs.Place_taylorRem_mem_toValuationSubring.ProofAuxJetT1.evalAt_sub_of_mem'

Source context 5 commands

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

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

Lean source · statement

theorem evalAt_sub_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'

L39 ↗

AlgebraicCurves.Places.Proofs.Place_taylorRem_mem_toValuationSubring.ProofAuxJetT1.ord_nonneg_of_mem'

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_taylorRem_mem_toValuationSubring
open AlgebraicCurve AlgebraicCurve.Place
namespace ProofAuxJetT1
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

sub_evalAt_mul_inv_mem'

L43 ↗

AlgebraicCurves.Places.Proofs.Place_taylorRem_mem_toValuationSubring.ProofAuxJetT1.sub_evalAt_mul_inv_mem'

Source context 5 commands

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

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

Lean source · statement

theorem sub_evalAt_mul_inv_mem' (v : Place K F) (hv : v.IsRational) {t : F} (ht : v.ord t = 1)
    {g : F} (hg : g ∈ v.toValuationSubring) :
    (g - algebraMap K F (v.evalAt g)) * t⁻¹ ∈ v.toValuationSubring

theorem

taylorRem_mem_toValuationSubring

L63 ↗

AlgebraicCurve.Place.taylorRem_mem_toValuationSubring

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_taylorRem_mem_toValuationSubring
open AlgebraicCurve AlgebraicCurve.Place

Lean source · statement

theorem _root_.AlgebraicCurve.Place.taylorRem_mem_toValuationSubring
    {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) (r : ℕ) :
    taylorRem v t f r ∈ v.toValuationSubring

Module documentation

Place taylor Rem mem to Valuation Subring

Declarations

evalAt_sub_of_mem'

ord_nonneg_of_mem'

sub_evalAt_mul_inv_mem'

taylorRem_mem_toValuationSubring