Theorems · Theorem · commutative algebra

IsDiscreteValuationRing.ideal_eq_span_pow_irreducible

∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [IsDiscreteValuationRing R] {s : Ideal R},
  s ≠ ⊥ → ∀ {ϖ : R}, Irreducible ϖ → ∃ n, s = Ideal.span {ϖ ^ n}

Every nonzero ideal in a DVR is a power of the maximal ideal. See idealOrderIsoENat for a precise classification of ideals in a DVR.

Defined in

Mathlib.RingTheory.DiscreteValuationRing.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainIsDiscreteValuationRing