OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentByAbelianRationalDimension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Rational dimension of finitely generated nilpotent-by-abelian groups

Finite rational kernel abelianization is equivalent to a uniform rational homology bound for the ambient group. The implication from FP-infinity is not assumed or supplied by this equivalence.

  1. theorem OAI.PolycyclicRecognition.nilpotentByAbelian_rational_dimension_iff_kernel_rank line 20
  2. theorem OAI.PolycyclicRecognition.nilpotentByAbelian_mod_torsion_finite_dimension_of_rational_bound line 33