Integral elements over the ring of integers of a valution #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The ring of integers is integrally closed inside the original ring.
theorem
valuation.integers.mem_of_integral
{R : Type u}
{Γ₀ : Type v}
[comm_ring R]
[linear_ordered_comm_group_with_zero Γ₀]
{v : valuation R Γ₀}
{O : Type w}
[comm_ring O]
[algebra O R]
(hv : v.integers O)
{x : R}
(hx : is_integral O x) :
@[protected]
theorem
valuation.integers.integral_closure
{R : Type u}
{Γ₀ : Type v}
[comm_ring R]
[linear_ordered_comm_group_with_zero Γ₀]
{v : valuation R Γ₀}
{O : Type w}
[comm_ring O]
[algebra O R]
(hv : v.integers O) :
integral_closure O R = ⊥
theorem
valuation.integers.integrally_closed
{K : Type u}
{Γ₀ : Type v}
[field K]
[linear_ordered_comm_group_with_zero Γ₀]
{v : valuation K Γ₀}
{O : Type w}
[comm_ring O]
[is_domain O]
[algebra O K]
[is_fraction_ring O K]
(hv : v.integers O) :