OAI/GroupTheory/PolycyclicRecognition/Algebra/TorsionMatrixExponent.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A common exponent from a finite set of torsion eigenvalues

Finite-order matrices have separable minimal polynomials in characteristic zero. Thus a common period of their eigenvalues is a period of the matrices themselves, without a bound on the individual orders as an extra hypothesis.

  1. theorem OAI.PolycyclicRecognition.torsion_matrix_power_eq_one_of_roots line 19
  2. theorem OAI.PolycyclicRecognition.common_exponent_of_torsion_matrix_roots line 44