Module

Place_taylorCoeff_ord_ne_zero.lean

Nyll.AlgebraicCurves.Places.Place_taylorCoeff_ord_ne_zero

3 declarations indexed from sourceView source ↗

Module documentation

Place taylor Coeff ord ne zero

Imports5

Imported by1

Nyll.AlgebraicCurves.Places.All

theorem

evalAt_eq_zero_of_ord_pos

L33 ↗

AlgebraicCurves.Places.Proofs.Place_taylorCoeff_ord_ne_zero.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_taylorCoeff_ord_ne_zero
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

L46 ↗

AlgebraicCurves.Places.Proofs.Place_taylorCoeff_ord_ne_zero.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_taylorCoeff_ord_ne_zero
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

taylorCoeff_ord_ne_zero

L55 ↗

AlgebraicCurve.Place.taylorCoeff_ord_ne_zero

Source context 4 commands

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

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

Lean source · statement

theorem _root_.AlgebraicCurve.Place.taylorCoeff_ord_ne_zero
    {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) :
    taylorCoeff v t (v.ord f).toNat f ≠ 0

Module documentation

Place taylor Coeff ord ne zero

Declarations

evalAt_eq_zero_of_ord_pos

ord_mul_inv_pow

taylorCoeff_ord_ne_zero