Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-02-15 18:15
76621bb7
View on Github →
feat: closed subgroup of profinite group is intersection of open subgroups containing it (
#34785
)
Estimated changes
Modified
Mathlib/Topology/Algebra/ClopenNhdofOne.lean
added
theorem
ProfiniteGrp.closedSubgroup_eq_sInf_open
modified
theorem
ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one