mathlib documentation

ring_theory.valuation.integral

Integral elements over the ring of integers of a valution #

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) :
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) :