NYLL
Module

Place_ord_nonneg_of_mem.lean

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

Module documentation

Place ord nonneg of mem

A function in the valuation subring of a place has nonnegative order.

Imports1
Imported by46

Declarations

theorem

rowMain

L40 ↗
AlgebraicCurves.Places.Place_ord_nonneg_of_mem.AlgebraicCurve.Place.rowMain
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Place_ord_nonneg_of_mem
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 rowMain {f : F} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f
theorem

ord_nonneg_of_mem

L62 ↗
AlgebraicCurve.Place.ord_nonneg_of_mem
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Place_ord_nonneg_of_mem
open IsDedekindDomain WithZero IsLocalRing
open _root_.AlgebraicCurve _root_.AlgebraicCurves.Places.Place_ord_nonneg_of_mem.AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.ord_nonneg_of_mem {K F : Type*} [Field K] [Field F]
  [Algebra K F] (v : Place K F) {f : F} (hf : 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.