Module

Place_forall_lt_taylorCoeff_eq_zero_iff_le_ord.lean

Nyll.AlgebraicCurves.Places.Place_forall_lt_taylorCoeff_eq_zero_iff_le_ord

3 declarations indexed from sourceView source ↗

Module documentation

Place forall lt taylor Coeff eq zero iff le ord

Imports4

Imported by3

theorem

evalAt_eq_zero_of_ord_pos

L32 ↗

AlgebraicCurves.Places.Proofs.Place_forall_lt_taylorCoeff_eq_zero_iff_le_ord.ProofAuxJetT2.evalAt_eq_zero_of_ord_pos

Source context 6 commands

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

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

Lean source · statement

theorem evalAt_eq_zero_of_ord_pos (v : Place K F) {g : F} (hg0 : g ≠ 0) (hpos : 0 < v.ord g) :
    v.evalAt g = 0

theorem

ord_mul_inv_pow

L45 ↗

AlgebraicCurves.Places.Proofs.Place_forall_lt_taylorCoeff_eq_zero_iff_le_ord.ProofAuxJetT2.ord_mul_inv_pow

Source context 6 commands

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

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

Lean source · statement

theorem ord_mul_inv_pow (v : Place K F) {t f : F} (ht0 : t ≠ 0) (hf0 : f ≠ 0) (ht : v.ord t = 1)
    (q : ℕ) : v.ord (f * t⁻¹ ^ q) = v.ord f - q

theorem

forall_lt_taylorCoeff_eq_zero_iff_le_ord

L54 ↗

AlgebraicCurve.Place.forall_lt_taylorCoeff_eq_zero_iff_le_ord

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_forall_lt_taylorCoeff_eq_zero_iff_le_ord
open AlgebraicCurve AlgebraicCurve.Place
open ProofAuxJetT2 in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.forall_lt_taylorCoeff_eq_zero_iff_le_ord
    {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) (hf0 : f ≠ 0) (e : ℕ) :
    (∀ q, q < e → taylorCoeff v t q f = 0) ↔ (e : ℤ) ≤ v.ord f

Module documentation

Place forall lt taylor Coeff eq zero iff le ord

Declarations

evalAt_eq_zero_of_ord_pos

ord_mul_inv_pow

forall_lt_taylorCoeff_eq_zero_iff_le_ord