OAI/GroupTheory/PolycyclicRecognition/Finiteness/FiniteStabilizerSumVanishing.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Direct sums of the finite-stabilizer rational coefficients

The integral projective dimension bound is uniform, so arbitrary direct sums still have projective dimension at most one. No countability or finiteness-presentation hypothesis is needed for this base case.

  1. theorem OAI.PolycyclicRecognition.integralRepresentationSum_projectiveDimension_one line 20
  2. theorem OAI.PolycyclicRecognition.finiteStabilizerSum_projectiveDimension_one line 44
  3. theorem OAI.PolycyclicRecognition.finiteStabilizerSum_completeCohomology line 51