OAI/GroupTheory/PolycyclicRecognition/Algebra/LocallyBoundedDerivedSeries.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A uniform derived-series bound passes from finitely generated subgroups

  1. def OAI.PolycyclicRecognition.ambientDerivedSeries line 12
  2. theorem OAI.PolycyclicRecognition.ambientDerivedSeries_mono line 15
  3. theorem OAI.PolycyclicRecognition.ambientDerivedSeries_zero line 22
  4. theorem OAI.PolycyclicRecognition.ambientDerivedSeries_succ line 25
  5. def OAI.PolycyclicRecognition.fgDerivedSubgroup line 29
  6. theorem OAI.PolycyclicRecognition.derivedSeries_le_fgDerivedSubgroup line 41
  7. theorem OAI.PolycyclicRecognition.derivedSeries_eq_bot_of_fg_subgroups line 63