OAI/GroupTheory/PolycyclicRecognition/Finiteness/NormalExtensionHomologyVanishing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Homological vanishing for a normal extension

The explicit second-page comparison and the finite diagonal filtration give the required additive bound for integral homology, with its hypotheses visible.

  1. theorem OAI.PolycyclicRecognition.normalExtension_homology_isZero_of_secondPage line 17
  2. theorem OAI.PolycyclicRecognition.normalExtension_homology_isZero_above line 33