Commit 2023-03-04 08:58 cd0354b1

View on Github →

feat: port CategoryTheory.Limits.Unit (#2597)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Unit.lean

added def CategoryTheory.Limits.pUnitCocone

added def CategoryTheory.Limits.pUnitCoconeIsColimit

added def CategoryTheory.Limits.pUnitCone

added def CategoryTheory.Limits.pUnitConeIsLimit