Theorem CommGrp.ofHom_injective

Modification history

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