English
If every prime ideal of a commutative semiring is principal, then every ideal is principal; i.e., the ring is a principal ideal ring.
Русский
Если каждый простый идеал коммутативного кольца является главным, то и каждый идеал является главным; то есть кольцо является кольцом с главными идеалами.
LaTeX
$$$$\text{If } R \text{ is commutative and } (\forall P\, (P \text{ prime} \Rightarrow P \text{ principal}))\; \Rightarrow\; (\forall I\, I \text{ is principal}).$$$$
Lean4
/-- If all prime ideals in a commutative ring are principal, so are all other ideals. -/
theorem of_prime (H : ∀ P : Ideal R, P.IsPrime → P.IsPrincipal) : IsPrincipalIdealRing R :=
by
refine ⟨isOka_isPrincipal.forall_of_forall_prime (fun I hI ↦ exists_maximal_not_isPrincipal ?_) H⟩
rw [isPrincipalIdealRing_iff, not_forall]
exact ⟨I, hI⟩
