OAI/GroupTheory/PolycyclicRecognition/Finiteness/NormalHomologyQuotient.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The quotient action on normal-subgroup homology

  1. theorem OAI.PolycyclicRecognition.normalHomologyMap_subgroup line 14
  2. def OAI.PolycyclicRecognition.quotientHomologyAction line 26