OAI/GroupTheory/PolycyclicRecognition/Algebra/TorsionEigenvaluesUnipotentPower.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A common unipotent power from torsion eigenvalues

A finite product synchronizes the eigenvalue periods. The split characteristic polynomial then divides a power of X^m - 1; evaluating at the operator proves nilpotence without choosing a Jordan basis.

  1. theorem OAI.PolycyclicRecognition.finite_torsion_common_power line 19
  2. theorem OAI.PolycyclicRecognition.split_polynomial_dvd_power_of_vanishing line 35
  3. theorem OAI.PolycyclicRecognition.unipotent_power_of_torsion_eigenvalues line 44