ProCGroups.FiniteGeneration

2 sections | 2 files | 81 declarations

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

Basic

1 files | 21 declarations | 18 Theorem | 3 Definition

Finitely generated as a topological group.

A countable descending chain of open characteristic subgroups. This packages the standard bounded-index characteristic-chain data.