Module

Place_mem_of_ord_nonneg.lean

Nyll.AlgebraicCurves.Places.Place_mem_of_ord_nonneg

2 declarations indexed from sourceView source ↗

Module documentation

Place mem of ord nonneg

A nonzero function of nonnegative order belongs to the valuation subring of a place.

Imports1

Nyll.AlgebraicCurves.Divisors.ClassGroup

Imported by42

theorem

rowMain

L40 ↗

AlgebraicCurves.Places.Place_mem_of_ord_nonneg.AlgebraicCurve.Place.rowMain

Source context 11 commands

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

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

theorem

mem_of_ord_nonneg

L55 ↗

AlgebraicCurve.Place.mem_of_ord_nonneg

Source context 4 commands