Source: ProCGroups

1import ProCGroups.Abelian

2import ProCGroups.Categorical

3import ProCGroups.Completion

4import ProCGroups.Duality

5import ProCGroups.FiniteGeneration

6import ProCGroups.FiniteGroups

7import ProCGroups.FiniteStepSolvableQuotients

8import ProCGroups.Frattini

9import ProCGroups.FreeConstructions

10import ProCGroups.FreeProC

11import ProCGroups.FreeProducts

12import ProCGroups.Generation

13import ProCGroups.GroupTheory

14import ProCGroups.InverseSystems

15import ProCGroups.LocalWeight

16import ProCGroups.NormalSubgroups

17import ProCGroups.Order

18import ProCGroups.Presentations

19import ProCGroups.ProC

20import ProCGroups.Profinite

21import ProCGroups.Topologies

22import ProCGroups.WreathProducts

23import ProCGroups.ReidemeisterSchreier

24import ProCGroups.CompletedGroupAlgebra

25import ProCGroups.FoxDifferential

26import ProCGroups.CrowellExactSequence

28/-!

29# Pro-C groups

31Reusable formalization of profinite and pro-\(C\) groups. The library covers finite-group

32classes, inverse systems and completions, free pro-\(C\) groups and products, generation,

33presentations, duality, topologies, and wreath products.

35`ProCGrp C` is the full subcategory of `ProfiniteGrp` cut out by the open-normal finite-quotient

36basis condition for `C`; its categorical and concrete structures are inherited from Mathlib.

37`FiniteGroupClass` includes finiteness and invariance under multiplicative equivalence, so the

38corresponding finite-group object property is isomorphism-invariant without extra hypotheses.

40This public aggregate imports every maintained Pro-C Groups component, including the

41Reidemeister--Schreier, completed group algebra, Fox differential, and Crowell exact-sequence

42layers.