Commit 2023-05-26 00:36 54c883d9

View on Github →

feat: port Algebra.Category.Group.Colimits (#3217)

Estimated changes

Modified Mathlib.lean

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

added def AddCommGroupCat.Colimits.ColimitType

added inductive AddCommGroupCat.Colimits.Prequotient

added inductive AddCommGroupCat.Colimits.Relation

added def AddCommGroupCat.Colimits.coconeFun

added def AddCommGroupCat.Colimits.coconeMorphism

added theorem AddCommGroupCat.Colimits.cocone_naturality

added theorem AddCommGroupCat.Colimits.cocone_naturality_components

added def AddCommGroupCat.Colimits.colimit

added def AddCommGroupCat.Colimits.colimitCocone

added def AddCommGroupCat.Colimits.colimitCoconeIsColimit

added def AddCommGroupCat.Colimits.colimitSetoid

added def AddCommGroupCat.Colimits.descFun

added def AddCommGroupCat.Colimits.descFunLift

added def AddCommGroupCat.Colimits.descMorphism

added theorem AddCommGroupCat.Colimits.quot_add

added theorem AddCommGroupCat.Colimits.quot_neg

added theorem AddCommGroupCat.Colimits.quot_zero