ProCGroups.FiniteStepSolvableQuotients

3 sections | 9 files | 147 declarations

This module formalizes finite-step solvable quotients and their abelian actions.

AbelianActions

3 files | 60 declarations | 48 Theorem | 12 Definition

An action has no nontrivial fixed points if every globally fixed element is trivial.

1 files | 14 declarations | 10 Theorem | 4 Definition

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

The topological closure of the abstract commutator subgroup.