Integral elements over the ring of integers of a valuation #
The ring of integers is integrally closed inside the original ring.
theorem
Valuation.Integers.mem_of_integral
{R : Type u}
{Γ₀ : Type v}
[CommRing R]
[LinearOrderedCommGroupWithZero Γ₀]
{v : Valuation R Γ₀}
{O : Type w}
[CommRing O]
[Algebra O R]
(hv : Valuation.Integers v O)
{x : R}
(hx : IsIntegral O x)
:
x ∈ Valuation.integer v
theorem
Valuation.Integers.integralClosure
{R : Type u}
{Γ₀ : Type v}
[CommRing R]
[LinearOrderedCommGroupWithZero Γ₀]
{v : Valuation R Γ₀}
{O : Type w}
[CommRing O]
[Algebra O R]
(hv : Valuation.Integers v O)
:
integralClosure O R = ⊥
theorem
Valuation.Integers.integrallyClosed
{K : Type u}
{Γ₀ : Type v}
[Field K]
[LinearOrderedCommGroupWithZero Γ₀]
{v : Valuation K Γ₀}
{O : Type w}
[CommRing O]
[Algebra O K]
[IsFractionRing O K]
(hv : Valuation.Integers v O)
: