OAI/GroupTheory/PolycyclicRecognition/Algebra/CayleyWordLength.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The shortest-word length for the fixed symmetric generating set

  1. theorem OAI.PolycyclicRecognition.wordBall_exhaustive line 14
  2. def OAI.PolycyclicRecognition.cayleyWordLength line 33
  3. theorem OAI.PolycyclicRecognition.cayleyWordLength_le_iff line 37
  4. theorem OAI.PolycyclicRecognition.cayleyWordLength_mul_le line 45
  5. theorem OAI.PolycyclicRecognition.cayleyWordLength_generator_le line 53
  6. theorem OAI.PolycyclicRecognition.cayleyWordLength_edge_difference line 59