Theorem Module.exists_surjective_quotient_of_finite

Modification history

2024-11-14 10:43
Mathlib/RingTheory/Finiteness.lean
chore(RingTheory): split Finiteness.lean into many smaller files (#18964) …
Modified Module.exists_surjective_quotient_of_finiteView on Github →
2024-11-06 15:34
Mathlib/RingTheory/Finiteness.lean
feat(Algebra/Category): for ring homs, epi + finite => surjective (#18267)
Added Module.exists_surjective_quotient_of_finiteView on Github →