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.