OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanSuffixGeneratorSequence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Actual generator chains attached to an arbitrary allowed sheet suffix

  1. theorem OAI.PolycyclicRecognition.CartanWordModel.exists_cartan_suffix_generator_sequence line 28

    Source documentation

    A box increment is generated inside an arbitrary allowed suffix, with one error envelope for all resulting sheet prefixes. The generation and ambient box templates may differ, as in the three probe paths in the neighboring-offset argument.

    theorem exists_cartan_suffix_generator_sequence
    [Nonempty (Fin M.letterCount)]
    (hExpG : IsGroupExponential ExpG)
    (realize : ExponentialLinearRealizationInput (EG := EG) (G := G))
…

    Mentions: OAI.PolycyclicRecognition.ExponentialLinearRealizationInput