Theorem Submodule.fg_iff_exists_finite_generating_family

Modification history

2024-11-14 10:43
Mathlib/RingTheory/Finiteness.lean
chore(RingTheory): split Finiteness.lean into many smaller files (#18964) …
Modified Submodule.fg_iff_exists_finite_generating_familyView on Github →
2024-11-02 13:54
Mathlib/RingTheory/Finiteness.lean
feat(Algebra/Module): relation between Module.FinitePresentation and Module.Presentation (#18408) …
Added Submodule.fg_iff_exists_finite_generating_familyView on Github →