NYLL
Module

Place_evalAt_eq_zero_iff_one_le_ord.lean

Nyll.AlgebraicCurves.Places.Place_evalAt_eq_zero_iff_one_le_ord
2 declarations indexed from sourceView source ↗

Module documentation

Place eval At eq zero iff one le ord

Imports1
Imported by2

Declarations

theorem

ord_nonnegative_of_mem

L25 ↗
AlgebraicCurves.Places.Proofs.Place_evalAt_eq_zero_iff_one_le_ord.ord_nonnegative_of_mem
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_eq_zero_iff_one_le_ord
open IsLocalRing AlgebraicCurve
Lean source · statement
theorem ord_nonnegative_of_mem {K F : Type*} [Field K] [Field F] [Algebra K F]
    (x : Place K F) {f : F} (hf : f ∈ x.toValuationSubring) : 0 ≤ x.ord f
theorem

evalAt_eq_zero_iff_one_le_ord

L44 ↗
AlgebraicCurve.Place.evalAt_eq_zero_iff_one_le_ord
Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_evalAt_eq_zero_iff_one_le_ord
open IsLocalRing AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.Place.evalAt_eq_zero_iff_one_le_ord {K F : Type*} [Field K] [Field F]
  [Algebra K F]
    (x : Place K F) (hx : x.IsRational) {f : F} (hf0 : f ≠ 0)
    (hf : f ∈ x.toValuationSubring) : x.evalAt f = 0 ↔ 1 ≤ x.ord f

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.