ProCGroups.GroupTheory

3 sections | 3 files | 45 declarations

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

CentralizerNormalizerCommensurator

1 files | 35 declarations | 29 Theorem | 4 Abbreviation | 2 Instance

The centralizer of a set of elements.

1 files | 4 declarations | 2 Theorem | 2 Definition

An automorphism descends to the quotient by a characteristic subgroup.

1 files | 6 declarations | 2 Theorem | 3 Definition | 1 Inductive

H is normal in K as an ambient subgroup relation.