OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteOrderUnipotent.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A rational unipotent operator of finite order is the identity

The polynomial X^n-1 is squarefree in characteristic zero. An operator it annihilates is semisimple, and its nilpotent difference from the identity must therefore vanish.

  1. theorem OAI.PolycyclicRecognition.rationalUnipotent_eq_one_of_pow_eq_one line 17