FenchelNielsenZomorrodian

2 sections | 93 files | 951 declarations

This module formalizes the Fenchel--Nielsen--Zomorrodian theorem. It currently uses two explicit local axioms for the finite-subgroup frontier. Reference: arXiv:2605.02577.

Discrete

This module formalizes the discrete group-theoretic part of the Fenchel--Nielsen--Zomorrodian theorem.

Profinite

This module formalizes the profinite part of the Fenchel--Nielsen--Zomorrodian theorem and uses the named local axiom frontier.