OAI/GroupTheory/PolycyclicRecognition/Algebra/CommonEigencharacterTorsion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Torsion characters of common eigenspaces

A nonzero common eigenspace gives a genuine character into the units of the field. If each operator has a unipotent positive power, this character has finite image on a finitely generated group.

  1. theorem OAI.PolycyclicRecognition.commonEigenspace_units_character line 18
  2. theorem OAI.PolycyclicRecognition.eigenvalue_torsion_of_unipotent_power line 48
  3. theorem OAI.PolycyclicRecognition.commonEigenspace_finite_character line 62