mathlib documentation

category_theory.groupoid.basic

This file defines a few basic properties of groupoids.

A subgroupoid is totally disconnected if it only has loops.

Equations