OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentFiniteTailBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A finite tail in a nilpotent lower central series has bounded length

  1. theorem OAI.PolycyclicRecognition.lowerCentralSeries_succ_lt_of_ne_bot line 11
  2. theorem OAI.PolycyclicRecognition.lowerCentralSeries_eq_bot_of_finite_tail line 30
  3. theorem OAI.PolycyclicRecognition.nilpotencyClass_le_quotient_add_finite_kernel line 56