OAI/GroupTheory/PolycyclicRecognition/Algebra/RationalSolvableDimension.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite virtual integral dimension modulo the finite normal radical

The nilpotent radical is selected using rational dimension and the bound on finite subgroup orders. No integral dimension of the ambient group is assumed.

  1. theorem OAI.PolycyclicRecognition.nilpotent_normal_torsionFree_of_no_finite_normal line 22
  2. theorem OAI.PolycyclicRecognition.solvable_rational_virtual_finite_dimension_of_no_finite_normal line 40
  3. theorem OAI.PolycyclicRecognition.solvable_rational_mod_finite_radical_dimension line 75