mathlib3 documentation

ring_theory.valuation.integral

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