Commit 2023-05-24 09:36 ac81fdb4

View on Github →

feat: port Algebra.Category.Group.FilteredColimits (#4274)

Estimated changes

Modified Mathlib.lean

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

added def CommGroupCat.FilteredColimits.colimitCoconeIsColimit

added theorem GroupCat.FilteredColimits.G.mk_eq

added def GroupCat.FilteredColimits.colimitCoconeIsColimit

added def GroupCat.FilteredColimits.colimitInvAux

added theorem GroupCat.FilteredColimits.colimitInvAux_eq_of_rel

added theorem GroupCat.FilteredColimits.colimit_inv_mk_eq