OAI/GroupTheory/PolycyclicRecognition/Algebra/InnerBarTranslation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

An augmented bar-resolution lift of inner conjugation

  1. theorem OAI.PolycyclicRecognition.bar_d_single_single line 15
  2. def OAI.PolycyclicRecognition.innerBarFreeMap line 30
  3. theorem OAI.PolycyclicRecognition.innerBarFreeMap_single line 35
  4. theorem OAI.PolycyclicRecognition.innerBarFreeMap_d line 44
  5. def OAI.PolycyclicRecognition.innerBarMap line 65
  6. theorem OAI.PolycyclicRecognition.innerBarMap_augmentation line 69
  7. def OAI.PolycyclicRecognition.innerBarMapHomotopy line 85