OAI/GroupTheory/PolycyclicRecognition/Algebra/AbelianCyclicFiniteDimension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Integral dimension for torsion-free abelian-by-infinite-cyclic groups of type FP∞

The rational rank bound is obtained from the actual second homology of the kernel, then used in the countable-union dimension argument.

  1. theorem OAI.PolycyclicRecognition.abelian_cyclic_kernel_finite_rank line 21
  2. theorem OAI.PolycyclicRecognition.abelian_infiniteCyclic_finite_dimension line 35