OAI/GroupTheory/PolycyclicRecognition/Algebra/RationalRecognitionEndgame.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Recognition from virtual solvability and the proved rational bounds

A finite normal subgroup is removed before duality transfer. Polycyclicity then lifts across that finite kernel. No virtual integral dimension of the original group is assumed in this argument.

  1. theorem OAI.PolycyclicRecognition.virtuallyPolycyclic_of_coarse_rational_bounds line 20