Structure OpenNormalAddSubgroup

Modification history

2024-10-04 10:12
Mathlib/Topology/Algebra/OpenSubgroup.lean
feat(Topology/Group): Open normal subgroup (#16980) …
Added OpenNormalAddSubgroupView on Github →