OAI/GroupTheory/PolycyclicRecognition/Algebra/IntegerConjugationUnipotent.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Unipotent powers of integral conjugation actions

For a finite free abelian quotient of a normal subgroup, integrality and splitting of the eigenvalues are constructed from the characteristic polynomial. They are not extra spectral hypotheses.

  1. theorem OAI.PolycyclicRecognition.dual_end_charpoly line 20
  2. theorem OAI.PolycyclicRecognition.integer_tensor_unit_span line 28
  3. theorem OAI.PolycyclicRecognition.polynomial_growth_integer_conjugation_unipotent_power line 46