ReidemeisterSchreier/Profinite/OpenSubgroups/Basic.lean

1import ProCGroups.GroupTheory.Subgroups

3/-

4PUBLIC_PAGE_SNAPSHOT

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

6lean_source: lean4/ReidemeisterSchreier/Profinite/OpenSubgroups/Basic.lean

7translation_root: data/translation

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

9placement: after imports, never before imports

11/-!

12# Profinite open-subgroup Schreier theory

14Profinite open subgroup quotients, finite permutation targets, dense free models, exact right Schreier generation, and topological rank bounds.

17open scoped Topology Pointwise

20open ProCGroups

21open ProCGroups.GroupTheory

23universe u v

25/-!

26# Profinite open-subgroup basics

28This module now only re-exports general rank and subgroup-relation helpers

29from `ProCGroups` for RS profinite files. RS-specific open-subgroup theorems

30live in the more focused files under this directory.