OAI/GroupTheory/PolycyclicRecognition/Algebra/TorsionSpectrumFiniteTrace.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite traces from torsion spectra

The matrices need not themselves have finite order. Only their eigenvalues are assumed to be roots of unity. In an irreducible finitely generated linear group this forces the whole group to be finite.

  1. theorem OAI.PolycyclicRecognition.finite_trace_of_torsion_spectra line 17
  2. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.finite_of_irreducible_fg_torsion_spectra line 51
  3. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.infinite_irreducible_fg_has_nontorsion_eigenvalue line 64