OAI/GroupTheory/PolycyclicRecognition/Finiteness/AbelianCyclicFinitenessEndgame.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The FP-infinity finiteness endgame for abelian-by-cyclic groups

The kernel need not be finitely generated. Its torsion and all prime-field reductions are controlled by the ambient finite projective resolutions.

  1. theorem OAI.PolycyclicRecognition.abelian_cyclic_kernel_characteristic_finiteIndex_torsionFree line 21
  2. theorem OAI.PolycyclicRecognition.abelian_cyclic_virtual_finite_dimension line 31