Theorems · Theorem · commutative algebra

ValuationRing.of_integers

∀ {𝒪 : Type u} {K : Type v} {Γ : Type w} [inst : CommRing 𝒪] [inst_1 : Field K] [inst_2 : Algebra 𝒪 K]
  [inst_3 : LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ) (hh : v.Integers 𝒪), ValuationRing 𝒪

If 𝒪 satisfies v.integers 𝒪 where v is a valuation on a field, then 𝒪 is a valuation ring.

Defined in

Mathlib.RingTheory.Valuation.ValuationRing

Cited by

1 results in Mathlib

Foundations

Depth 47 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingFieldAlgebraLinearOrderedCommGroupWithZero