ProCGroups.Order

1 sections | 1 files | 41 declarations

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

Basic

1 files | 41 declarations | 24 Theorem | 9 Definition | 8 Instance

Closed subgroups have a top element: the whole group.