OAI/GroupTheory/PolycyclicRecognition/Algebra/SolvableLinearStructure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A finite-index subgroup with nilpotent derived group

The topology used here is the concrete polynomial topology pulled back along a faithful representation. Its connected component has finite index. No algebraic-group structure theorem is assumed.

  1. theorem OAI.PolycyclicRecognition.PolynomialMatrixGroup.exists_finiteIndex_nilpotent_commutator_of_injective line 21
  2. theorem OAI.PolycyclicRecognition.FiniteRationalLinearModel.exists_finiteIndex_nilpotent_commutator line 52