Commit 2025-09-30 12:06 9d2bcc53

View on Github →

feat(RingTheory): golf IsPrincipalIdealRing.of_prime (#28477) In complement to #28451 and as discussed in #27200, this PR uses the newly added Oka predicates to golf the proof of IsPrincipalIdealRing.of_prime.

Estimated changes

Modified Mathlib/RingTheory/PrincipalIdealDomain.lean

added theorem Ideal.exists_maximal_not_isPrincipal

added theorem Ideal.nonPrincipals_eq_empty_iff

added theorem Ideal.nonPrincipals_zorn

modified theorem nonPrincipals_def

modified theorem nonPrincipals_eq_empty_iff

modified theorem nonPrincipals_zorn

Modified Mathlib/RingTheory/PrincipalIdealDomainOfPrime.lean

added theorem Ideal.isOka_isPrincipal