Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Def
category_theory.groupoid.of_hom_unique
Modification history
2022-03-17 01:38
src/category_theory/groupoid.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.groupoid.of_hom_unique
View on Github →