OAI/GroupTheory/PolycyclicRecognition/Algebra/SolvableSubgroupFiniteExtension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A solvable normal subgroup with finite index in the height kernel

  1. theorem OAI.PolycyclicRecognition.quotientImage_finite_of_relative_finiteIndex line 11
  2. theorem OAI.PolycyclicRecognition.virtuallySolvable_of_relative_finiteIndex_solvable line 26