Theorem smul_connectedComponent

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 smul_connectedComponent View on Github →