OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanSubexponentialGroupChain.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual group chains joining allowed suffixes

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_subexponential_group_chain line 31

    Source documentation

    Both the vertices and the individual generator steps lie in one subexponential enlargement of the original group box. The time estimate uses precisely the original support width.

    theorem exists_subexponential_group_chain
    [Nonempty (Fin M.letterCount)]
    (hExp : IsGroupExponential Exp)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput