English
Let v be a valuation on K and 𝒪 a subring of K such that every element of 𝒪 has integral valuation with respect to v. Then 𝒪 is a valuation ring of K.
Русский
Пусть v — валиация на K и 𝒪 подкольцо K такое, что каждый элемент 𝒪 имеет целочисленную величину по отношению к v. Тогда 𝒪 является валюационным кольцом над K.
LaTeX
$$$\mathcal{O} \text{ является валюационным кольцом над } K \quad\text{если} \quad v(\mathcal{O}) \subseteq \mathbb{Z}_{\ge 0}$$$
Lean4
/-- If `𝒪` satisfies `v.integers 𝒪` where `v` is a valuation on a field, then `𝒪`
is a valuation ring. -/
theorem of_integers (v : Valuation K Γ) (hh : v.Integers 𝒪) :
haveI := hh.hom_inj.isDomain
ValuationRing 𝒪 :=
by
haveI := hh.hom_inj.isDomain
suffices PreValuationRing 𝒪 from .mk
constructor
intro a b
rcases le_total (v (algebraMap 𝒪 K a)) (v (algebraMap 𝒪 K b)) with h | h
· obtain ⟨c, hc⟩ := Valuation.Integers.dvd_of_le hh h
use c; exact Or.inr hc.symm
· obtain ⟨c, hc⟩ := Valuation.Integers.dvd_of_le hh h
use c; exact Or.inl hc.symm
