Valuation subring is integrally closed

theorem Valuation.Integers.isIntegral_iff_v_le_one {R : Type u_1} {Γ₀ : Type u_3} {O : Type u_4} [CommRing R] [LinearOrderedCommGroupWithZero Γ₀] [CommRing O] [Algebra O R] {v : Valuation R Γ₀} (hv : v.Integers O) {x : R} : IsIntegral O x ↔ v x ≤ 1

theorem Valuation.Integers.isIntegrallyClosed {F : Type u_2} {Γ₀ : Type u_3} {O : Type u_4} [Field F] [LinearOrderedCommGroupWithZero Γ₀] [CommRing O] [Algebra O F] {v : Valuation F Γ₀} (hv : v.Integers O) : IsIntegrallyClosed O

instance Valuation.isIntegrallyClosed_integers {F : Type u_2} {Γ₀ : Type u_3} [Field F] [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation F Γ₀) : IsIntegrallyClosed ↥v.integer