Theorems · Theorem · commutative algebra

Ideal.eq_span_singleton_of_mem_of_notMem_sq_of_notMem_prime_ne

∀ {R : Type u_1} [inst : CommRing R] {P : Ideal R},
  P.IsPrime →
    ∀ [IsDedekindDomain R] {x : R},
      x ∈ P → x ∉ P ^ 2 → (∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q) → P = Ideal.span {x}

Let P be a prime ideal, x ∈ P \ P² and x ∉ Q for all prime ideals Q ≠ P. Then P is generated by x.

Defined in

Mathlib.RingTheory.DedekindDomain.PID

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsDedekindDomain