OAI/GroupTheory/PolycyclicRecognition/Algebra/GroupedGoodWords.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Successful switch words remain good at every bundle boundary

  1. theorem OAI.PolycyclicRecognition.wordSheetsGood_append_iff line 13
  2. theorem OAI.PolycyclicRecognition.WordSheetsGood.grouped line 24
  3. theorem OAI.PolycyclicRecognition.ofFn_eq_flatten_bundles line 34
  4. theorem OAI.PolycyclicRecognition.WordSheetsGood.bundle_products line 47
  5. theorem OAI.PolycyclicRecognition.WordSheetsGood.prefix_states line 56