OAI/GroupTheory/PolycyclicRecognition/Finiteness/NilpotentReducedCohomology.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Vanishing of reduced first cohomology for nilpotent groups

Induct on the nilpotency class through the quotient by the center, using the orthogonal central decomposition and the explicit central averaging step.

  1. theorem OAI.PolycyclicRecognition.unitaryReducedVanishing_nilpotent line 18
  2. theorem OAI.PolycyclicRecognition.reducedCohomologyInput_of_nilpotent line 29