Theorem Ideal.exists_maximal_not_isPrincipal

Modification history

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