Yamaguchi Lean 4 Library
ProCGroups.FiniteGroups
ProCGroups/FiniteGroups

ProCGroups.FiniteGroups

3 sections | 3 files | 128 declarations

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

AllFinite

1 files | 10 declarations | 8 Theorem | 1 Definition | 1 Instance
The class of all finite groups.

Classes

1 files | 60 declarations | 36 Theorem | 10 Definition | 1 Abbreviation | 8 Structure | 4 Class | 1 Instance
A class of groups, implemented as an unbundled predicate on group carriers.

StandardClasses

1 files | 58 declarations | 49 Theorem | 8 Definition | 1 Instance
If \(a \nmid b\), then some prime factor has a larger exponent in \(a\) than in \(b\).