NYLL
Module

Place_mem_iff_ord_nonneg.lean

Nyll.AlgebraicCurves.Places.Place_mem_iff_ord_nonneg
4 declarations indexed from sourceView source ↗

Module documentation

Place mem iff ord nonneg

A nonzero function belongs to the valuation subring of a place exactly when its order is nonnegative.

Imports1
Imported by45

Declarations

theorem

ord_nonneg_of_mem

L40 ↗
AlgebraicCurve.Place.ord_nonneg_of_mem
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Place_mem_iff_ord_nonneg
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ord_nonneg_of_mem {f : F} (hf :
  f ∈ v.toValuationSubring) : 0 ≤ v.ord f
theorem

mem_of_ord_nonneg

L57 ↗
AlgebraicCurve.Place.mem_of_ord_nonneg
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Place_mem_iff_ord_nonneg
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_of_ord_nonneg {f : F} (hf : f ≠ 0) (h :
  0 ≤ v.ord f) :
    f ∈ v.toValuationSubring
theorem

rowMain

L67 ↗
AlgebraicCurves.Places.Place_mem_iff_ord_nonneg.AlgebraicCurve.Place.rowMain
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Place_mem_iff_ord_nonneg
open IsDedekindDomain WithZero IsLocalRing
noncomputable section
namespace AlgebraicCurve
open _root_.AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
variable {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve.Place
Lean source · statement
theorem rowMain {f : F} (hf : f ≠ 0) :
    f ∈ v.toValuationSubring ↔ 0 ≤ v.ord f
theorem

mem_iff_ord_nonneg

L78 ↗
AlgebraicCurve.Place.mem_iff_ord_nonneg
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Place_mem_iff_ord_nonneg
open IsDedekindDomain WithZero IsLocalRing
open _root_.AlgebraicCurve _root_.AlgebraicCurves.Places.Place_mem_iff_ord_nonneg.AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.mem_iff_ord_nonneg {K F : Type*} [Field K] [Field F]
  [Algebra K F] (v : Place K F) {f : F} (hf : f ≠ 0) :
    f ∈ v.toValuationSubring ↔ 0 ≤ v.ord f

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