Theorem Module.fgSystem.equiv_comp_of

Modification history

2025-01-02 19:57
Mathlib/Algebra/Colimit/Finiteness.lean
feat(Algebra/Colimit): the directed system of finitely generated submodules (#20264) …
Added Module.fgSystem.equiv_comp_ofView on Github →