FenchelNielsenZomorrodian/Discrete/Singerman/KernelTransport.lean
1import FenchelNielsenZomorrodian.Discrete.Core.Signature
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Singerman/KernelTransport.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Singerman/Reidemeister-Schreier bridge
14Cyclic quotient actions, cyclic product identities, Schreier kernel computations, free-group word identities, and kernel transport for the compact Fuchsian proof.
15-/
17namespace FenchelNielsen
19 {ι : Type*} {ρ : ι → ℕ}
20 (n : ∀ i : ι, Fin (ρ i) → ℕ) :
21 (Σ i : ι, Fin (ρ i)) → ℕ
22 | ⟨i, k⟩ => n i k
23end FenchelNielsen