OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteOrderMatrixTraces.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite trace sets for matrices with a common finite exponent

Every trace is a sum of a fixed number of roots from one finite set. Combined with irreducibility and the trace pairing this proves finiteness.

  1. theorem OAI.PolycyclicRecognition.finite_trace_of_charpoly_roots_subset line 17
  2. theorem OAI.PolycyclicRecognition.charpoly_root_power_eq_one line 33
  3. theorem OAI.PolycyclicRecognition.finite_trace_of_common_matrix_exponent line 52
  4. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.finite_of_irreducible_common_exponent line 64