Theorem Ideal.isOka_isPrincipal

Modification history

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