OAI/GroupTheory/PolycyclicRecognition/Algebra/ConjugateWindowStabilization.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A stable finite window of cyclic conjugates

Polynomial word growth rules out strict growth at every conjugate window. This is the finite-generation step for the kernel of a cyclic quotient.

  1. def OAI.PolycyclicRecognition.conjugateWindow line 16
  2. def OAI.PolycyclicRecognition.conjugateWindowSubgroup line 19
  3. theorem OAI.PolycyclicRecognition.conjugateWindow_mono line 22
  4. theorem OAI.PolycyclicRecognition.conjugateWindowSubgroup_mono line 30
  5. theorem OAI.PolycyclicRecognition.pow_mem_wordBall line 35
  6. theorem OAI.PolycyclicRecognition.zpow_mem_wordBall line 43
  7. theorem OAI.PolycyclicRecognition.conjugateWindow_word_bound line 50
  8. theorem OAI.PolycyclicRecognition.exists_stable_conjugate_window line 65