Commit 2023-03-23 17:36 b1d3f2ca

View on Github →

feat: port Algebra.Category.Group.Basic (#3036)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/GroupCat/Basic.lean

added def AddCommGroupCat.asHom

added theorem AddCommGroupCat.asHom_apply

added theorem AddCommGroupCat.asHom_injective

added theorem AddCommGroupCat.injective_of_mono

added theorem AddCommGroupCat.int_hom_ext

added def CategoryTheory.Aut.isoPerm

added def CategoryTheory.Aut.mulEquivPerm

added def CategoryTheory.Iso.commGroupIsoToMulEquiv

added def CategoryTheory.Iso.groupIsoToMulEquiv

added theorem CommGroupCat.Hom.map_mul

added theorem CommGroupCat.Hom.map_one

added def CommGroupCat.Hom.mk

added theorem CommGroupCat.Hom.mk_apply

added theorem CommGroupCat.coe_of

added theorem CommGroupCat.comp_apply

added theorem CommGroupCat.ext

added theorem CommGroupCat.id_apply

added def CommGroupCat.of

added def CommGroupCat.ofHom

added theorem CommGroupCat.ofHom_apply

added theorem CommGroupCat.one_apply

added def CommGroupCat

added theorem GroupCat.Hom.map_mul

added theorem GroupCat.Hom.map_one

added def GroupCat.Hom.mk

added theorem GroupCat.Hom.mk_apply

added theorem GroupCat.coe_of

added theorem GroupCat.comp_apply

added theorem GroupCat.ext

added theorem GroupCat.id_apply

added def GroupCat.of

added def GroupCat.ofHom

added theorem GroupCat.ofHom_apply

added theorem GroupCat.one_apply

added def GroupCat

added def MulEquiv.toCommGroupCatIso

added def MulEquiv.toGroupCatIso

added def mulEquivIsoCommGroupIso

added def mulEquivIsoGroupIso

Modified Mathlib/Algebra/Category/MonCat/Basic.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/Basic.lean