ProCGroups/FiniteGeneration.lean

1import ProCGroups.FiniteGeneration.Basic

2import ProCGroups.FiniteGeneration.CharacteristicChainsAndIndices

4/-

5PUBLIC_PAGE_SNAPSHOT

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

7lean_source: lean4/ProCGroups/FiniteGeneration.lean

8translation_root: data/translation

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

10placement: after imports, never before imports

12/-!

13# Finite generation and characteristic chains

15Records finite generation criteria for profinite groups, finite-index/open-subgroup counting, characteristic cores, and index bounds.