Def CategoryTheory.Groupoid.IsTotallyDisconnected

Modification history

2023-02-17 10:44
Mathlib/CategoryTheory/Groupoid/Basic.lean
feat: port CategoryTheory.Groupoid.Basic (#2335)
Added CategoryTheory.Groupoid.IsTotallyDisconnectedView on Github →