THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines a few basic properties of groupoids.
theorem category_theory.groupoid.is_thin_iff (C : Type u_1) [category_theory.groupoid C] :
quiver.is_thin C ↔ ∀ (c : C), subsingleton (c ⟶ c)
def category_theory.groupoid.is_totally_disconnected (C : Type u_1) [category_theory.groupoid C] :
A subgroupoid is totally disconnected if it only has loops.