Commit 2023-06-10 00:02 b31b2034

View on Github →

feat: port CategoryTheory.Closed.Zero (#4921)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Closed/Zero.lean

added def CategoryTheory.equivPunit

added def CategoryTheory.uniqueHomsetOfInitialIsoTerminal

added def CategoryTheory.uniqueHomsetOfZero