Commit 2023-06-17 05:05 59f83749

View on Github →

feat: port CategoryTheory.Monoidal.Internal.Limits (#5150)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean

added def Mon_.forgetMapConeLimitConeIso

added def Mon_.limit

added def Mon_.limitCone

added def Mon_.limitConeIsLimit