ProCGroups/Completion.lean

1import ProCGroups.Completion.FiniteQuotientLifts

2import ProCGroups.Completion.FiniteQuotientSystems

3import ProCGroups.Completion.ProCGroupAlgebra

4import ProCGroups.Completion.ProCInteger

5import ProCGroups.Completion.ProCIntegerPrimePower

6import ProCGroups.Completion.SameFiniteQuotients

7import ProCGroups.Completion.UniversalProperty

9/-

10PUBLIC_PAGE_SNAPSHOT

11generated_at: 2026-05-27T09:47:29+09:00

12lean_source: lean4/ProCGroups/Completion.lean

13translation_root: data/translation

14purpose: identifies the local data snapshot used to build pages/

15placement: after imports, never before imports

17/-!

18# ProCGroups.Completion

20Wrapper for the `ProCGroups.Completion` folder.