Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-05-21 15:13
357f2822
View on Github →
feat: port Algebra.Category.Mon.FilteredColimits (
#4094
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Algebra/Category/Mon/FilteredColimits.lean
added
def
CommMonCat.FilteredColimits.colimitCoconeIsColimit
added
theorem
MonCat.FilteredColimits.M.mk_eq
added
def
MonCat.FilteredColimits.coconeMorphism
added
theorem
MonCat.FilteredColimits.cocone_naturality
added
def
MonCat.FilteredColimits.colimitCoconeIsColimit
added
def
MonCat.FilteredColimits.colimitDesc
added
theorem
MonCat.FilteredColimits.colimitMulAux_eq_of_rel_left
added
theorem
MonCat.FilteredColimits.colimitMulAux_eq_of_rel_right
added
theorem
MonCat.FilteredColimits.colimit_mul_mk_eq
added
theorem
MonCat.FilteredColimits.colimit_one_eq
Modified
Mathlib/Algebra/Category/MonCat/Basic.lean