ProCGroups/Generation.lean
1import ProCGroups.Generation.Basic
2import ProCGroups.Generation.Convergence
3import ProCGroups.Generation.GeneratorConvergingPairs
4import ProCGroups.Generation.QuotientCriteria
5import ProCGroups.Generation.QuotientGeneratorConvergingPairs
6import ProCGroups.Generation.WordProductsAndClosure
8/-
9PUBLIC_PAGE_SNAPSHOT
10generated_at: 2026-05-27T09:47:29+09:00
11lean_source: lean4/ProCGroups/Generation.lean
12translation_root: data/translation
13purpose: identifies the local data snapshot used to build pages/
14placement: after imports, never before imports
15-/
16/-!
17# Topological generation
19Develops topological generation, generating families, convergence-to-one criteria, quotient generation, and profinite generation lemmas.
20-/