OAI/GroupTheory/PolycyclicRecognition/Geometry/RootCoreExtensionDimension.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The finite-dimensional nilpotent-by-abelian step

Only an actual finite root core in the nilpotent kernel and a finite-rank torsion-free abelian quotient are used. No cohomological dimension premise for the kernel or ambient group is needed.

  1. theorem OAI.PolycyclicRecognition.finiteDimension_of_nilpotent_rootCore_abelian_quotient line 18