Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Theorem
category_theory.equiv_punit_iff_unique
Modification history
2022-03-17 01:38
src/category_theory/punit.lean
feat(category_theory/punit): A groupoid is equivalent to punit iff it has a unique arrow between any two objects (#12726) …
Added
category_theory.equiv_punit_iff_unique
View on Github →