Module

Place_canonicalLocalResidueDataK_eq.lean

Nyll.AlgebraicCurves.Places.Place_canonicalLocalResidueDataK_eq

3 declarations indexed from sourceView source ↗

Module documentation

Place canonical Local Residue Data K eq

Imports5

Imported by1

Nyll.AlgebraicCurves.Places.All

theorem

evalAt_add'

L39 ↗

AlgebraicCurves.Places.Proofs.Place_canonicalLocalResidueDataK_eq.AlgebraicCurve.Place.S8b.evalAt_add'

Source context 11 commands

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

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

Lean source · statement

theorem evalAt_add' (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

res_eq_of_le_ord

L47 ↗

AlgebraicCurves.Places.Proofs.Place_canonicalLocalResidueDataK_eq.AlgebraicCurve.Place.S8b.res_eq_of_le_ord

Source context 11 commands

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

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

Lean source · statement

theorem res_eq_of_le_ord (v : Place K F) (hv : v.IsRational) (d₁ d₂ : v.CanonicalLocalResidueDataK)
  :
    ∀ n : ℕ, ∀ f : F, f ≠ 0 → -(n : ℤ) ≤ v.ord f → d₁.res f = d₂.res f

theorem

canonicalLocalResidueDataK_eq

L100 ↗

AlgebraicCurve.Place.canonicalLocalResidueDataK_eq

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_canonicalLocalResidueDataK_eq
open _root_.AlgebraicCurve
open AlgebraicCurve.Place.S8b in

Lean source · statement

theorem _root_.AlgebraicCurve.Place.canonicalLocalResidueDataK_eq
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : Place K F) (hv : v.IsRational) (d₁ d₂ : v.CanonicalLocalResidueDataK) :
    d₁ = d₂

Module documentation

Place canonical Local Residue Data K eq

Declarations

evalAt_add'

res_eq_of_le_ord

canonicalLocalResidueDataK_eq