Def OpenNormalSubgroup.pathComponentOne

Modification history

2025-06-10 20:04
Mathlib/Topology/Connected/PathComponentOne.lean
feat: add path component of the identity in a locally path connected topological group, as an open normal subgroup (#25668)
Added OpenNormalSubgroup.pathComponentOneView on Github →