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