OAI/GroupTheory/PolycyclicRecognition/Algebra/ConnectedSolvableUnipotence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform unipotence of the commutator action

Successive common eigenspaces of a connected solvable matrix action are fixed by its commutator subgroup. Induction on the quotient dimension therefore makes every sufficiently long mixed product of commutator action differences zero.

  1. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.connected_solvable_commutator_words line 25