OAI/GroupTheory/PolycyclicRecognition/Geometry/RootCoreAbelianRank.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Abelian subgroups of nilpotent groups with a finite root core

A finitely generated core meets every abelian subgroup in a finitely generated subgroup with the same rational span. No torsion-free hypothesis is needed for this rank statement.

  1. theorem OAI.PolycyclicRecognition.nilpotent_rootCore_abelian_subgroup_finite line 18