Commit 2025-01-16 12:40 84b31f65

View on Github →

feat(Topology/Group/Profinite): Profinite group is limit of finite group (#16992) Prove that any profinite group is limit of finite groups.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Subgroup/Basic.lean

added theorem Subgroup.normal_iInf_normal

Modified Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean

Created Mathlib/Topology/Algebra/Category/ProfiniteGrp/Limits.lean

added theorem ProfiniteGrp.denseRange_toLimit

added def ProfiniteGrp.toFiniteQuotientFunctor

added def ProfiniteGrp.toLimit

added def ProfiniteGrp.toLimit_fun

added theorem ProfiniteGrp.toLimit_fun_continuous

added theorem ProfiniteGrp.toLimit_injective

added theorem ProfiniteGrp.toLimit_surjective

Modified Mathlib/Topology/Algebra/ClopenNhdofOne.lean

added theorem ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhd_of_one

Modified Mathlib/Topology/Algebra/OpenSubgroup.lean