OAI/GroupTheory/PolycyclicRecognition/Algebra/CharacteristicCentralTransgression.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual transgression for a characteristic central subgroup

  1. def OAI.PolycyclicRecognition.subgroupQuotientExtension line 14
  2. theorem OAI.PolycyclicRecognition.subgroupQuotientExtension_central line 23
  3. def OAI.PolycyclicRecognition.characteristicCentralTransgressionIntertwining line 28
  4. def OAI.PolycyclicRecognition.characteristicCentralTransgression line 40
  5. theorem OAI.PolycyclicRecognition.characteristicCentralTransgression_exact_H2 line 48
  6. theorem OAI.PolycyclicRecognition.characteristicCentralTransgression_exact_kernel line 56