OAI/GroupTheory/PolycyclicRecognition/Finiteness/AbelianNormalFinitenessEndgame.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

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

No finite generation, rank, or torsion-free hypothesis is imposed on the abelian kernel. These are the actual finite projective resolution consequences.

  1. theorem OAI.PolycyclicRecognition.abelian_normal_virtual_finite_dimension line 22