Documentation
Mathlib
.
Algebra
.
Category
.
Grp
.
Subobject
Search
Google site search
return to top
source
Imports
Init
Mathlib.Algebra.Category.Grp.ZModuleEquivalence
Mathlib.Algebra.Category.ModuleCat.Subobject
Imported by
AddCommGrp
.
wellPowered_addCommGrp
The category of abelian groups is well-powered
#
source
instance
AddCommGrp
.
wellPowered_addCommGrp
:
CategoryTheory.WellPowered
AddCommGrp
Equations
AddCommGrp.wellPowered_addCommGrp
=
⋯