OAI/GroupTheory/PolycyclicRecognition/Algebra/GromovLinearReduction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The linear-group reduction in the polynomial-growth theorem

The explicit parameter below is the real-matrix specialization of Tits, Free subgroups in linear groups, J. Algebra 20 (1972), Theorem 1, p.250. Combined with harmonic representations, degree reduction, and solvable polynomial-growth estimates, it gives virtual nilpotence.

  1. theorem OAI.PolycyclicRecognition.polynomial_growth_virtual_integer_quotient_of_linearStep line 24
  2. theorem OAI.PolycyclicRecognition.IsVirtuallyPolycyclic.exists_solvable_finiteDimension line 57
  3. theorem OAI.PolycyclicRecognition.polynomial_growth_virtually_nilpotent_degree_of_linearStep line 66
  4. theorem OAI.PolycyclicRecognition.gromovPolynomialGrowthInput_of_linearStep line 109