OAI/GroupTheory/PolycyclicRecognition/Algebra/CentralDerivedTransgression.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A central derived layer is a quotient of actual second homology

  1. theorem OAI.PolycyclicRecognition.characteristicCentralTransgression_surjective line 14
  2. theorem OAI.PolycyclicRecognition.normalCentralDerived_finite_of_quotient_H2_finite line 29