OAI/GroupTheory/PolycyclicRecognition/Algebra/FiniteNormalGeneration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Finite normal generators over an abelian quotient

A finitely generated ambient group supplies finitely many normal generators for every normal subgroup with abelian quotient. This prepares the finite group-ring module in the nilpotent-by-abelian finiteness argument.

  1. theorem OAI.PolycyclicRecognition.commutator_le_normal_of_generators line 20
  2. theorem OAI.PolycyclicRecognition.commutator_finitelyNormallyGenerated line 50
  3. theorem OAI.PolycyclicRecognition.finitelyNormallyGenerated_of_commutator_le line 62
  4. theorem OAI.PolycyclicRecognition.finitelyNormallyGenerated_of_abelian_quotient line 82