Documentation
Mathlib
.
CategoryTheory
.
Groupoid
.
Discrete
Search
return to top
source
Imports
Init
Mathlib.CategoryTheory.Groupoid
Mathlib.CategoryTheory.Discrete.Basic
Imported by
CategoryTheory
.
instGroupoidDiscrete
Discrete categories are groupoids
#
source
instance
CategoryTheory
.
instGroupoidDiscrete
{
C
:
Type
u_1}
:
Groupoid
(
Discrete
C
)
Equations
One or more equations did not get rendered due to their size.