FenchelNielsenZomorrodian/Discrete.lean
1import FenchelNielsenZomorrodian.Discrete.Abelianization.EllipticAbelianization
2import FenchelNielsenZomorrodian.Discrete.Abelianization.PeriodClassOrder
3import FenchelNielsenZomorrodian.Discrete.Abelianization.PeriodCoordinate
4import FenchelNielsenZomorrodian.Discrete.Abelianization.PeriodQuotient
5import FenchelNielsenZomorrodian.Discrete.Arithmetic.FamilyLcm
6import FenchelNielsenZomorrodian.Discrete.Arithmetic.FinsetLcm
7import FenchelNielsenZomorrodian.Discrete.Arithmetic.PrimeDivisors
8import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.AbelianizationKernel.Conditions
9import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.AbelianizationKernel.Periods
10import FenchelNielsenZomorrodian.Discrete.MainTheorem
11import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.FirstReduction.Signatures
12import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodFamilies
13import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodOne.LowCardDihedral
14import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodOne.SourceSubgroup
15import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodOne.TargetSignatures
16import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.Quotients
17import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.SecondReduction.OrderedTargetSignature
18import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.SecondReduction.Signatures
19import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.ZeroGenus.Perfectness
20import FenchelNielsenZomorrodian.Discrete.Coordinates.FenchelPeriodCoordinate
21import FenchelNielsenZomorrodian.Discrete.Coordinates.ZModFamily
22import FenchelNielsenZomorrodian.Discrete.Core.CompactFuchsianPresentation
23import FenchelNielsenZomorrodian.Discrete.Core.EllipticCompact
24import FenchelNielsenZomorrodian.Discrete.Core.EllipticQuotientHom
25import FenchelNielsenZomorrodian.Discrete.Core.FamilySignature
26import FenchelNielsenZomorrodian.Discrete.Core.Signature
27import FenchelNielsenZomorrodian.Discrete.FiniteIndex.Definitions
28import FenchelNielsenZomorrodian.Discrete.FiniteIndex.KernelTransfer
29import FenchelNielsenZomorrodian.Discrete.FiniteIndex.NormalCore
30import FenchelNielsenZomorrodian.Discrete.FiniteIndex.Smooth
31import FenchelNielsenZomorrodian.Discrete.FiniteIndex.SmoothQuotientData
32import FenchelNielsenZomorrodian.Discrete.GroupTheory.Basic
33import FenchelNielsenZomorrodian.Discrete.GroupTheory.DerivedSeries
34import FenchelNielsenZomorrodian.Discrete.Singerman.CyclicProductIdentities
35import FenchelNielsenZomorrodian.Discrete.Singerman.CyclicQuotientActions
36import FenchelNielsenZomorrodian.Discrete.Singerman.CyclicSchreierKernel
37import FenchelNielsenZomorrodian.Discrete.Singerman.FreeGroupWords
38import FenchelNielsenZomorrodian.Discrete.Singerman.KernelTransport
39import FenchelNielsenZomorrodian.Discrete.Singerman.ReidemeisterSchreier
40import FenchelNielsenZomorrodian.Discrete.Torsion.CompactFiniteOrder
41import FenchelNielsenZomorrodian.Discrete.Torsion.FuchsianFiniteSubgroupFrontier
43/-
44PUBLIC_PAGE_SNAPSHOT
45generated_at: 2026-05-27T09:47:29+09:00
46lean_source: lean4/FenchelNielsenZomorrodian/Discrete.lean
47translation_root: data/translation
48purpose: identifies the local data snapshot used to build pages/
49placement: after imports, never before imports
50-/
51/-!
52# FenchelNielsenZomorrodian.Discrete
54Public wrapper for the reusable discrete FNZ API: arithmetic, signatures, abelianization,
55period-coordinate data, quotient data, torsion frontiers, and the discrete main theorem used by
56the profinite bridge. Reduction proof data, relator proof certificates, and transport maps remain
57available through focused imports.
58-/