OAI/GroupTheory/PolycyclicRecognition/Finiteness/FiniteIndexFiniteness.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Integral FP finiteness is invariant under finite index

The reverse direction uses the proved coarse filling theorem. The necessary finite-generation hypotheses are derived from FP one and coset representatives.

  1. theorem OAI.PolycyclicRecognition.group_fg_of_finiteIndex line 18
  2. theorem OAI.PolycyclicRecognition.typeFP_finiteIndex_iff line 37
  3. theorem OAI.PolycyclicRecognition.typeFPInfinity_finiteIndex_iff line 49
  4. theorem OAI.PolycyclicRecognition.IsIntegralPoincareDualityGroup.finiteIndex_subgroup line 54