Yamaguchi Lean 4 Library
ProCGroups.ProC.GroupPredicates
ProCGroups/ProC/GroupPredicates

ProCGroups.ProC.GroupPredicates

3 sections | 3 files | 109 declarations

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

Abelian

1 files | 1 declarations | 1 Theorem
Every pro-abelian group is abelian.

Basic

1 files | 78 declarations | 33 Theorem | 30 Definition | 2 Abbreviation | 2 Structure | 9 Class | 2 Instance
The all-finite pro-\(C\) predicate is profiniteness.

Standard

1 files | 30 declarations | 11 Theorem | 10 Definition | 9 Instance
On finite discrete groups, the finite quotient class induced by \(\mathrm{finiteGroupClassProCPredicate}\,C\) recovers \(C\), provided \(C\) is quotient- and isomorphism-closed.