OAI/GroupTheory/PolycyclicRecognition/Finiteness/HeightKernelCoefficientDimension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finite dimension of the coefficient ring for the height-kernel extension

The kernel may contain torsion and its finitely generated subgroups may have unbounded ranks. The quotient alone is assumed to have finite integral dimension.

  1. theorem OAI.PolycyclicRecognition.TypeFPInfinity.heightKernel_smallCoefficient_vanishing line 18
  2. theorem OAI.PolycyclicRecognition.TypeFPInfinity.heightKernel_smallCoefficient_finite_dimension line 27