Theorem Ideal.nonPrincipals_zorn

Modification history

2025-09-30 12:06
Mathlib/RingTheory/PrincipalIdealDomain.lean
feat(RingTheory): golf `IsPrincipalIdealRing.of_prime` (#28477) …
Added Ideal.nonPrincipals_zornView on Github →