OAI/GroupTheory/PolycyclicRecognition/Algebra/ValuedEigenlineFreePair.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Free powers after a change of normed coefficient field

Concrete spectral gaps and transverse eigenlines imply free powers over the coefficient field. This is the dynamical part needed for Tits's field change.

  1. theorem OAI.PolycyclicRecognition.ValuedLinearDynamics.free_powers_of_dominant_eigenlines line 19
  2. theorem OAI.PolycyclicRecognition.ValuedLinearDynamics.free_powers_of_transverse_eigenline_cones line 65
  3. theorem OAI.PolycyclicRecognition.ValuedLinearDynamics.free_powers_of_transverse_dominant_eigenlines line 137