Theorem Module.DirectLimit.exists_of₂

Modification history

2024-12-26 06:54
Mathlib/Algebra/Colimit/ModuleRing.lean
feat(Algebra/Colimit/ModuleRing): generalize to Semiring/AddCommMonoid (#20212) …
Added Module.DirectLimit.exists_of₂View on Github →