Commit 2023-02-23 08:11 6c48d9a5

View on Github →

feat: Port CategoryTheory.Bicategory.End (#2454)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Bicategory/End.lean

added def CategoryTheory.EndMonoidal