OAI/GroupTheory/PolycyclicRecognition/Algebra/AdmissibleGeneratorWords.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Generator words whose entire path stays in an open set

  1. def OAI.PolycyclicRecognition.generatorWordBase line 18
  2. theorem OAI.PolycyclicRecognition.isOpen_generatorWordBase line 24
  3. theorem OAI.PolycyclicRecognition.generatorWordBase_subset line 34
  4. theorem OAI.PolycyclicRecognition.eventually_short_flowLineBase line 42
  5. theorem OAI.PolycyclicRecognition.eventually_prefix_generatorWordBase line 58
  6. theorem OAI.PolycyclicRecognition.eq_on_admissible_generatorWord line 72