Commit 2024-09-29 13:27 e17fd83d

View on Github →

feat(Topology/Group): define closed subgroup (#16977) Define the type of closed subgroup in a topological group.

Estimated changes

Modified Mathlib.lean

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

added theorem Subgroup.normalCore_eq_iInf_conjAct

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

added def ProfiniteGrp.ofClosedSubgroup

Created Mathlib/Topology/Algebra/ClosedSubgroup.lean

added structure ClosedAddSubgroup

added theorem ClosedSubgroup.toSubgroup_injective

added structure ClosedSubgroup

added theorem Subgroup.isOpen_of_isClosed_of_finiteIndex

added theorem Subgroup.normalCore_isClosed