OAI/GroupTheory/PolycyclicRecognition/Algebra/AlternatingWordOrder.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Chronological alternating words and the two polynomial input blocks

  1. def OAI.PolycyclicRecognition.alternatingWordIndex line 13
  2. theorem OAI.PolycyclicRecognition.alternatingWordIndex_left line 16
  3. theorem OAI.PolycyclicRecognition.alternatingWordIndex_right line 24
  4. def OAI.PolycyclicRecognition.alternatingWordBlockEquiv line 34
  5. theorem OAI.PolycyclicRecognition.alternatingWordBlockEquiv_left line 38
  6. theorem OAI.PolycyclicRecognition.alternatingWordBlockEquiv_right line 43
  7. theorem OAI.PolycyclicRecognition.alternatingWordBlockEquiv_apply line 48
  8. theorem OAI.PolycyclicRecognition.measurePreserving_alternatingWordBlockEquiv line 52
  9. theorem OAI.PolycyclicRecognition.alternatingWordBlockEquiv_image_measure line 58
  10. theorem OAI.PolycyclicRecognition.continuous_alternatingWordBlockEquiv line 68
  11. theorem OAI.PolycyclicRecognition.alternatingWordBlockEquiv_prod line 76