Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-11-10 11:25 ecbcd382

View on Github →

feat(category_theory/closed): cartesian closed category with zero object is trivial (#4924)

Estimated changes

Created src/category_theory/closed/zero.lean

added def category_theory.equiv_punit

added def category_theory.unique_homset_of_initial_iso_terminal

added def category_theory.unique_homset_of_zero