OAI/GroupTheory/PolycyclicRecognition/Finiteness/SubgroupBarResolution.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Subgroup inclusions on the free bar resolution

  1. def OAI.PolycyclicRecognition.subgroupFreeInclusion line 15
  2. theorem OAI.PolycyclicRecognition.subgroupFreeInclusion_single line 19
  3. theorem OAI.PolycyclicRecognition.subgroupFreeInclusion_d line 32
  4. def OAI.PolycyclicRecognition.subgroupBarResolutionMap line 51
  5. theorem OAI.PolycyclicRecognition.barResolution_pi_single line 60
  6. theorem OAI.PolycyclicRecognition.subgroupBarResolutionMap_π line 89
  7. def OAI.PolycyclicRecognition.subgroupBarResolutionHomotopy line 107