OAI/GroupTheory/PolycyclicRecognition/Finiteness/FinitenessFromControlledFillings.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finiteness from uniformly controlled fillings

Finite group generation supplies the first augmentation kernel. Each further kernel is finite by the controlled-filling comparison, so the chosen projective cover remains finite through the required degree.

  1. theorem OAI.PolycyclicRecognition.typeFP_of_controlledCycleFillings line 20
  2. theorem OAI.PolycyclicRecognition.TypeFP.mono line 39