Module

Canonical.lean

Nyll.AlgebraicCurves.Differentials.Residues.Canonical

3 declarations indexed from sourceView source ↗

Module documentation

Results on Canonical.

Imports6

Imported by7

theorem

ord_nonneg_of_mem_loc

L165 ↗

AlgebraicCurve.Place.ord_nonneg_of_mem_loc

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)

Lean source · statement

theorem ord_nonneg_of_mem_loc {f : F} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f

theorem

mem_of_ord_nonneg_loc

L180 ↗

AlgebraicCurve.Place.mem_of_ord_nonneg_loc

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)

Lean source · statement

theorem mem_of_ord_nonneg_loc {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord f) :
    f ∈ v.toValuationSubring

theorem

mem_iff_ord_nonneg_loc

L188 ↗

AlgebraicCurve.Place.mem_iff_ord_nonneg_loc

Source context 6 commands

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

noncomputable section
open IsDedekindDomain WithZero Module IsLocalRing
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)

Lean source · statement

theorem mem_iff_ord_nonneg_loc {f : F} (hf : f ≠ 0) :
    f ∈ v.toValuationSubring ↔ 0 ≤ v.ord f

Module documentation

Declarations

ord_nonneg_of_mem_loc

mem_of_ord_nonneg_loc

mem_iff_ord_nonneg_loc