OAI/GroupTheory/PolycyclicRecognition/Algebra/ExpandingConjugationWords.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Expanding conjugation creates exponentially many short words

The character is an additive-valued homomorphism on a normal subgroup. Its expansion separates binary words in conjugates of a single element.

  1. def OAI.PolycyclicRecognition.conjugationBinaryWord line 16
  2. theorem OAI.PolycyclicRecognition.conjugationBinaryWord_character line 20
  3. theorem OAI.PolycyclicRecognition.conjugationBinaryWord_injective_length line 32
  4. theorem OAI.PolycyclicRecognition.conjugationBinaryWord_word_bound line 45
  5. theorem OAI.PolycyclicRecognition.expanding_conjugation_exponential_count line 64
  6. theorem OAI.PolycyclicRecognition.polynomial_growth_no_expanding_conjugation line 91