ProCGroups.FreeConstructions

3 sections | 3 files | 14 declarations

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

AmalgamsAndModules

1 files | 2 declarations | 2 Theorem

A finite nontrivial \(p\)-group has a nontrivial central element. This is the group-theoretic core used for finite normal subgroups in pro-\(p\) amalgam arguments.

FiniteSubgroupBounds

1 files | 3 declarations | 2 Theorem | 1 Structure

Data recording that a finite subgroup is conjugate into one of the two factor images.

Framework

1 files | 9 declarations | 9 Definition

A finite subgroup, formulated on an actual subgroup of an actual group.