Theorem Module.exists_isPrincipal_quotient_of_finite

Modification history

2025-03-05 15:27
Mathlib/RingTheory/Finiteness/TensorProduct.lean
chore(RingTheory): merge `Finiteness/TensorProduct.lean` into `TensorProduct/Finite.lean` (#22595) …
Modified Module.exists_isPrincipal_quotient_of_finiteView on Github →
2024-11-14 10:43
Mathlib/RingTheory/Finiteness.lean
chore(RingTheory): split Finiteness.lean into many smaller files (#18964) …
Modified Module.exists_isPrincipal_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_isPrincipal_quotient_of_finiteView on Github →