OAI/GroupTheory/PolycyclicRecognition/Algebra/PolycyclicExtensionDimension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Passing finite virtual dimension through a polycyclic quotient

  1. theorem OAI.PolycyclicRecognition.exists_solvable_finiteDimension_of_cyclicSeries line 12
  2. theorem OAI.PolycyclicRecognition.exists_solvable_finiteDimension_of_virtuallyPolycyclic_quotient line 43