Mathlib Changelog
v4
Changelog
About
Github
Theorem
totallyDisconnectedSpace_iff_connectedComponent_one
Modification history
2026-02-17 15:21
Mathlib/Topology/Algebra/Group/Basic.lean
feat(Topology/Algebra/Group/Basic): group is totally disconnected iff `connectedComponent 1 = {1}` (#35404) …
Added
totallyDisconnectedSpace_iff_connectedComponent_one
View on Github →