OAI/GroupTheory/PolycyclicRecognition/Finiteness/NoetherianResolutionHomology.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite homology over an abelian quotient group ring

This is the noetherian algebra step for a finite projective resolution after taking normal-subgroup coinvariants. The chain-level comparison is separate.

  1. theorem OAI.PolycyclicRecognition.integralAbelianGroupRing_noetherian line 18
  2. theorem OAI.PolycyclicRecognition.module_finite_shortComplex_homology line 22
  3. theorem OAI.PolycyclicRecognition.integralAbelianGroupRing_finite_homology line 32