OAI/GroupTheory/PolycyclicRecognition/Algebra/CyclicConjugateGeneration.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite generation of the full cyclic-conjugate subgroup

A stable finite conjugate window contains all integer conjugates. Combined with polynomial-growth stabilization, this is an actual finite-generation theorem, with no assumed kernel-finiteness input.

  1. def OAI.PolycyclicRecognition.cyclicConjugateSubgroup line 17
  2. theorem OAI.PolycyclicRecognition.cyclic_conjugation_add line 21
  3. theorem OAI.PolycyclicRecognition.conjugateWindow_conjugation line 27
  4. theorem OAI.PolycyclicRecognition.conjugateWindowSubgroup_conjugation line 38
  5. theorem OAI.PolycyclicRecognition.stable_conjugateWindow_eq_full line 53
  6. theorem OAI.PolycyclicRecognition.cyclicConjugateSubgroup_fg_of_polynomial_growth line 92