Theorem Module.DirectLimit.exists_eq_of_of_eq

Modification history

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