Yamaguchi Lean 4 Library
Homepage
Source: ProCGroups.FiniteGroups
ProCGroups
/
FiniteGroups
/
Source
Source: ProCGroups.FiniteGroups
1
import
ProCGroups.FiniteGroups.AllFinite
2
import
ProCGroups.FiniteGroups.StandardClasses
3
4
/-!
5
# Classes of finite groups
6
7
This aggregate module exposes the class of all finite groups together with the standard
8
formations, varieties, and closure properties used to define pro-`C` groups.
9
-/