OAI/GroupTheory/PolycyclicRecognition/Algebra/DualUnipotentPower.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Returning from dual eigenvalues to an actual unipotent power

Dual functionals separate vectors. Thus nilpotence detected on the dual is nilpotence of the original operator, with the same exponent.

  1. theorem OAI.PolycyclicRecognition.dual_end_pow line 17
  2. theorem OAI.PolycyclicRecognition.dual_end_sub line 25
  3. theorem OAI.PolycyclicRecognition.nilpotent_of_dual_nilpotent line 30
  4. theorem OAI.PolycyclicRecognition.unipotent_power_of_dual_torsion_eigenvalues line 42
  5. theorem OAI.PolycyclicRecognition.polynomial_growth_integral_conjugation_unipotent_power line 52