Commit 2023-05-21 13:59 a85cea98

View on Github →

feat: port Algebra.Category.Group.Limits (#4148)

Estimated changes

Modified Mathlib.lean

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

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

added def AddCommGroupCat.kernelIsoKer

added def AddCommGroupCat.kernelIsoKerOver

added theorem AddCommGroupCat.kernelIsoKer_hom_comp_subtype

added theorem AddCommGroupCat.kernelIsoKer_inv_comp_ι

added def GroupCat.sectionsSubgroup