OAI/GroupTheory/PolycyclicRecognition/Algebra/SolvableFiniteExtension.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Solvable finite extensions of polycyclic groups

Take the normal core of a polycyclic finite-index subgroup. Its quotient is finite and solvable, and thus has a cyclic series. The extension construction then gives a cyclic series for the original group.

  1. theorem OAI.PolycyclicRecognition.isPolycyclic_of_finite_solvable line 17
  2. theorem OAI.PolycyclicRecognition.IsVirtuallyPolycyclic.polycyclic_of_solvable line 20
  3. theorem OAI.PolycyclicRecognition.IsIntegralPoincareDualityGroup.polycyclic_of_virtuallyNilpotent line 29