OAI/GroupTheory/PolycyclicRecognition/Algebra/AbelianCyclicUnipotentNilpotence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Nilpotence of an abelian-by-cyclic group with unipotent action

The kernels of powers of the action difference lie in successive upper central terms. The integer quotient adds just one final central step.

  1. theorem OAI.PolycyclicRecognition.abelian_cyclic_kernel_mem_upperCentral line 17
  2. theorem OAI.PolycyclicRecognition.abelian_cyclic_nilpotent_of_unipotent line 58