FenchelNielsenZomorrodian/Discrete/Singerman/ReidemeisterSchreier.lean

1import ReidemeisterSchreier.Discrete.OpenSubgroups.ClassicalGeneratorBasis

3/-

4PUBLIC_PAGE_SNAPSHOT

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

6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Singerman/ReidemeisterSchreier.lean

7translation_root: data/translation

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

9placement: after imports, never before imports

11/-!

12# Singerman/Reidemeister-Schreier bridge

14Cyclic quotient actions, cyclic product identities, Schreier kernel computations, free-group word

15identities, and kernel transport for the compact Fuchsian proof.

18namespace FenchelNielsen

19export ReidemeisterSchreier.Discrete.OpenSubgroups (

21 schreierGenerator

30end FenchelNielsen