OAI/GroupTheory/PolycyclicRecognition/Finiteness/NilpotentNormalRationalHomology.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Rational homology for a finite-rank nilpotent normal kernel

The rank premise is retained. The proof supplies finite rational dimensions for the canonical derived quotient action and the actual extension homology; it does not deduce rank from ambient FP-infinity.

  1. theorem OAI.PolycyclicRecognition.nilpotentNormal_rationalDerived_finite line 23
  2. theorem OAI.PolycyclicRecognition.normalExtension_rational_secondPage_finite_of_kernel_rank line 30
  3. theorem OAI.PolycyclicRecognition.normalExtension_rational_homology_finite_of_kernel_rank line 36