OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteNormalRadical.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The largest finite normal subgroup under a finite-subgroup order bound

  1. theorem OAI.PolycyclicRecognition.finite_sup_of_normal line 12
  2. theorem OAI.PolycyclicRecognition.exists_largest_finite_normal line 21