ProCGroups.Profinite

3 sections | 3 files | 30 declarations

This module develops finite quotient, subgroup, free pro-\(C\), generation, and cardinal-invariant constructions for profinite and pro-\(C\) groups.

Basic

1 files | 15 declarations | 14 Theorem | 1 Definition

An unbundled profinite group is a compact Hausdorff totally disconnected topological group.

1 files | 4 declarations | 3 Theorem | 1 Definition

Every bundled profinite group is profinite in the working unbundled sense.

1 files | 11 declarations | 10 Theorem | 1 Definition

An open subgroup is open as a subset.