OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentByAbelianReduction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The concrete nilpotent-by-abelian subgroup for the duality endgame

  1. theorem OAI.PolycyclicRecognition.nilpotent_of_injective_hom line 10
  2. theorem OAI.PolycyclicRecognition.exists_finiteIndex_nilpotent_by_abelian line 15