Commit 2023-05-18 20:51 87c4a75e

View on Github →

feat: port Algebra.Category.Mon.Limits (#3073)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Category/MonCat/Basic.lean

modified theorem MonCat.forget_map

Created Mathlib/Algebra/Category/MonCat/Limits.lean

added def MonCat.HasLimits.limitCone

added def MonCat.HasLimits.limitConeIsLimit

added def MonCat.limitπMonoidHom

added def MonCat.sectionsSubmonoid

Modified Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

Modified Mathlib/Data/TypeMax.lean