Theorem ProfiniteGrp.closedSubgroup_eq_sInf_open

Modification history

2026-02-15 18:15
Mathlib/Topology/Algebra/ClopenNhdofOne.lean
feat: closed subgroup of profinite group is intersection of open subgroups containing it (#34785)
Added ProfiniteGrp.closedSubgroup_eq_sInf_openView on Github →