OAI/GroupTheory/PolycyclicRecognition/Algebra/VirtuallyUnipotentCommutatorAction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform commutator-action bounds after passing to finite index

This version retains the action bound even when the original representation has a kernel, as needed for conjugation on a nilpotent normal subgroup.

  1. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.exists_finiteIndex_commutator_words line 19
  2. theorem OAI.PolycyclicRecognition.exists_finiteIndex_rational_commutator_words line 51