Yamaguchi Lean 4 Library
FenchelNielsenZomorrodian.Discrete.CompactFuchsian.AbelianizationKernel
FenchelNielsenZomorrodian/Discrete/CompactFuchsian/AbelianizationKernel

FenchelNielsenZomorrodian.Discrete.CompactFuchsian.AbelianizationKernel

2 sections | 2 files | 9 declarations

Wrapper for the FenchelNielsenZomorrodian.Discrete.CompactFuchsian.AbelianizationKernel folder.

Conditions

1 files | 5 declarations | 5 Definition
The abelianization-kernel condition is rewritten as the corresponding finite presentation relation on elliptic and canonical generators.

Periods

1 files | 4 declarations | 4 Definition
The period family used to describe the abelianization-kernel condition.