ProCGroups.ProfiniteGrp.eq_one_of_mem_all_openNormalSubgroups
In a profinite group, an element lying in every open normal subgroup must be \(1\).
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open Set
open scoped Topology Pointwise
namespace ProCGroups
universe u
section Permanence
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace ProfiniteGrpLean source · statement
theorem eq_one_of_mem_all_openNormalSubgroups [CompactSpace G]
[TotallyDisconnectedSpace G] {x : G}
(hx : ∀ U : OpenNormalSubgroup G, x ∈ (U : Subgroup G)) : x = 1