Commit 2026-02-17 15:21 c6bb5a58
View on Github →feat(Topology/Algebra/Group/Basic): group is totally disconnected iff connectedComponent 1 = {1} (#35404)
This PR proves that a group G is totally disconnected if and only if connectedComponent 1 = {1}.