OAI/GroupTheory/PolycyclicRecognition/Finiteness/IntegralBarAugmentation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Augmentation and degenerate bar chains

  1. def OAI.PolycyclicRecognition.integralBarAugmentation line 11
  2. theorem OAI.PolycyclicRecognition.integralBarAugmentation_single line 14
  3. theorem OAI.PolycyclicRecognition.integralBarAugmentation_boundary line 20
  4. theorem OAI.PolycyclicRecognition.integralBarAugmentation_cycle line 33
  5. def OAI.PolycyclicRecognition.integralBarDegenerate line 37
  6. def OAI.PolycyclicRecognition.integralBarDegeneratePrimitive line 40
  7. theorem OAI.PolycyclicRecognition.integralBarDegenerate_single line 43
  8. theorem OAI.PolycyclicRecognition.integralBarDegenerate_boundary line 47