Theorem Module.DirectLimit.quotMk_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.quotMk_of View on Github →