OAI/GroupTheory/PolycyclicRecognition/Analysis/WordSupportPaths.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Concatenating the bounded generator word

The one-letter visit is applied on each successive height-zero sheet. The result is one continuous path to the whole word, with constants depending only on the bounded number of letters.

  1. theorem OAI.PolycyclicRecognition.exists_word_support_path line 20