Theorems · Theorem · commutative algebra

Ideal.nonPrincipals_zorn

∀ {R : Type u} [inst : Semiring R],
  ¬IsPrincipalIdealRing R →
    ∀ c ⊆ Ideal.nonPrincipals R, IsChain (fun x1 x2 => x1 ≤ x2) c → ∃ I ∈ Ideal.nonPrincipals R, ∀ J ∈ c, J ≤ I

Any chain in the set of non-principal ideals has an upper bound which is non-principal. (Namely, the union of the chain is such an upper bound.) If you want the existence of a maximal non-principal ideal see Ideal.exists_maximal_not_isPrincipal.

Defined in

Mathlib.RingTheory.PrincipalIdealDomain

Cited by

1 results in Mathlib

Foundations

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

Assumes

Semiring