Theorems · Theorem · commutative algebra

IsDedekindDomain.exists_sup_span_eq

∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R] {I J : Ideal R}, I ≤ J → I ≠ 0 → ∃ a, I ⊔ Ideal.span {a} = J

In a Dedekind domain, for every ideals 0 < I ≤ J there exists a such that J = I + ⟨a⟩. TODO: Show that this property uniquely characterizes Dedekind domains.

Defined in

Mathlib.RingTheory.DedekindDomain.Factorization

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomain