OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteSolvableDerivedBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Explicit derived-length bounds for finite soluble quotients

  1. theorem OAI.PolycyclicRecognition.finite_solvable_derivedSeries_card line 11
  2. theorem OAI.PolycyclicRecognition.normalCore_index_le_factorial line 31
  3. theorem OAI.PolycyclicRecognition.derivedSeries_add_le_ambient line 36
  4. theorem OAI.PolycyclicRecognition.solvable_derivedSeries_bound_of_finiteIndex line 44