OAI/GroupTheory/PolycyclicRecognition/Analysis/FiniteIndexQuasiUnipotentAction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite-index uniform unipotence of solvable actions

The identity component in the pulled-back polynomial matrix topology is normal and has finite index. The connected-action theorem applies to it. Faithfulness of the representation is not required.

  1. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.exists_finiteIndex_quasiUnipotent_words line 20