Commit 2023-05-23 10:39 b2a93020

View on Github →

feat: port Algebra.Category.Ring.Colimits (#4164)

Estimated changes

Modified Mathlib.lean

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

added def CommRingCat.Colimits.ColimitType

added inductive CommRingCat.Colimits.Prequotient

added inductive CommRingCat.Colimits.Relation

added def CommRingCat.Colimits.coconeFun

added def CommRingCat.Colimits.coconeMorphism

added theorem CommRingCat.Colimits.cocone_naturality

added theorem CommRingCat.Colimits.cocone_naturality_components

added def CommRingCat.Colimits.colimit

added def CommRingCat.Colimits.colimitCocone

added def CommRingCat.Colimits.colimitIsColimit

added def CommRingCat.Colimits.colimitSetoid

added def CommRingCat.Colimits.descFun

added def CommRingCat.Colimits.descFunLift

added def CommRingCat.Colimits.descMorphism

added theorem CommRingCat.Colimits.quot_add

added theorem CommRingCat.Colimits.quot_mul

added theorem CommRingCat.Colimits.quot_neg

added theorem CommRingCat.Colimits.quot_one

added theorem CommRingCat.Colimits.quot_zero