Theorems · Definition · Lie groups

OpenNormalSubgroup.toFiniteIndexNormalSubgroup

{G : Type u_1} →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] →
      [CompactSpace G] → [ContinuousMul G] → OpenNormalSubgroup G → FiniteIndexNormalSubgroup G

An open normal subgroup of a compact topological group has finite index.

Defined in

Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Cited by

2 results in Mathlib

Foundations

Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupTopologicalSpaceCompactSpaceContinuousMul