Theorem Ring.HasFiniteQuotients.of_module_finite

Modification history

2026-03-10 06:45
Mathlib/RingTheory/Ideal/Quotient/HasFiniteQuotients.lean
feat(RingTheory): add the class `HasFiniteQuotients` (#35530) …
Added Ring.HasFiniteQuotients.of_module_finiteView on Github →