OAI/GroupTheory/PolycyclicRecognition/Algebra/ConjugateEigenlineFreePair.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Free powers of a dominant element and a transverse conjugate

The conjugate has the same spectral gap, with a bounded change-of-coordinates constant. The power lemma absorbs that constant.

  1. theorem OAI.PolycyclicRecognition.linearRepresentation_cancel line 17
  2. theorem OAI.PolycyclicRecognition.linearRepresentation_conjugate line 23
  3. theorem OAI.PolycyclicRecognition.linearRepresentation_conjugate_vector line 28
  4. theorem OAI.PolycyclicRecognition.linearRepresentation_inverse_mem_line line 32
  5. theorem OAI.PolycyclicRecognition.free_powers_of_transverse_conjugate line 42