Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-06-11 13:19
45f44831
View on Github →
Port/Algebra.Category.Module.FilteredColimits (
#4949
)
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/Algebra/Category/GroupCat/FilteredColimits.lean
Created
Mathlib/Algebra/Category/ModuleCat/FilteredColimits.lean
added
theorem
ModuleCat.FilteredColimits.M.mk_eq
added
def
ModuleCat.FilteredColimits.coconeMorphism
added
def
ModuleCat.FilteredColimits.colimit
added
def
ModuleCat.FilteredColimits.colimitCocone
added
def
ModuleCat.FilteredColimits.colimitCoconeIsColimit
added
def
ModuleCat.FilteredColimits.colimitDesc
added
def
ModuleCat.FilteredColimits.colimitSmulAux
added
theorem
ModuleCat.FilteredColimits.colimitSmulAux_eq_of_rel
added
theorem
ModuleCat.FilteredColimits.colimit_smul_mk_eq
Modified
Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
modified
def
CategoryTheory.HasForget₂.mk'
modified
def
CategoryTheory.forget₂
modified
def
CategoryTheory.hasForgetToType