Theorem Ideal.isOka_fg

Modification history

2025-10-06 17:04
Mathlib/RingTheory/Noetherian/OfPrime.lean
feat(RingTheory/Noetherian): add `IsNoetherianRing.of_prime` (#28451) …
Added Ideal.isOka_fgView on Github →