OAI/GroupTheory/PolycyclicRecognition/Algebra/PolynomialGrowthNoFreePair.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Polynomial-growth groups contain no free pair

Positive words give the literal exponential counting obstruction needed for the linear-group alternative in the polynomial-growth argument.

  1. def OAI.PolycyclicRecognition.positiveFreeWord line 17
  2. theorem OAI.PolycyclicRecognition.positiveFreeWord_reduced line 20
  3. theorem OAI.PolycyclicRecognition.positiveFreeWord_injective line 31
  4. theorem OAI.PolycyclicRecognition.free_pair_exponential_word_count line 42
  5. theorem OAI.PolycyclicRecognition.polynomial_word_growth_not_exponential line 66
  6. theorem OAI.PolycyclicRecognition.polynomial_growth_no_free_pair line 95