Commit 2025-05-24 09:54 fe6ff4a5
View on Github →feat(CategoryTheory): IsDiscrete
implies IsGroupoid
(#25136)
Show the Prop
-class version of the fact that any discrete categories is a groupoid.
feat(CategoryTheory): IsDiscrete
implies IsGroupoid
(#25136)
Show the Prop
-class version of the fact that any discrete categories is a groupoid.