OAI/GroupTheory/PolycyclicRecognition/Algebra/CentralLayerAscendingBase.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A stable base in a central lower-central term

Commutators of a finitely generated lift provide the kernel base. Central errors disappear in positive lower-central terms, while the quotient exhaustion ensures that these commutators exhaust the actual kernel.

  1. theorem OAI.PolycyclicRecognition.exists_ascending_base_in_central_lowerCentral line 19
  2. theorem OAI.PolycyclicRecognition.exists_ascending_base_of_central_lowerCentral_quotient line 87