OAI/GroupTheory/PolycyclicRecognition/Analysis/GeneratorPrefixChain.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Fixed-length chains of actual generator prefixes

Words of length at most N are padded by zero-amplitude switches. This identifies the adjacent pairs to which the interior-switch theorem applies, while leaving the actual endpoint unchanged.

  1. def OAI.PolycyclicRecognition.generatorStepOrZero line 17
  2. theorem OAI.PolycyclicRecognition.generatorStepOrZero_bound line 20
  3. theorem OAI.PolycyclicRecognition.generatorGroupWord_prefix_step line 29
  4. theorem OAI.PolycyclicRecognition.generatorGroupWord_prefix_last line 44