Inductive Module.DirectLimit.Eqv

Modification history

2026-02-09 08:58
Mathlib/Algebra/Colimit/Module.lean
chore(style): remove duplicate instance hypotheses (#35002) …
Modified Module.DirectLimit.EqvView on Github →
2024-12-26 06:54
Mathlib/Algebra/Colimit/ModuleRing.lean
feat(Algebra/Colimit/ModuleRing): generalize to Semiring/AddCommMonoid (#20212) …
Added Module.DirectLimit.EqvView on Github →