OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentAbelianizationGenerators.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Generators lift from the abelianization of a nilpotent group

This does not require the group or the subgroup of lifts to be finitely generated. Central-quotient induction proves the generation statement.

  1. theorem OAI.PolycyclicRecognition.nilpotent_eq_top_of_sup_commutator line 17
  2. theorem OAI.PolycyclicRecognition.nilpotent_finitelyGenerated_of_abelianization line 46