Theorem AddCommGrp.isColimit_iff_bijective_desc

Modification history

2025-01-20 10:42
Mathlib/Algebra/Category/Grp/LargeColimits.lean
feat(Algebra/Category/Grp/LargeColimits): large colimits in the category of commutative additive groups (#20522) …
Added AddCommGrp.isColimit_iff_bijective_descView on Github →