OAI/GroupTheory/PolycyclicRecognition/Algebra/ListBarPairHomotopy.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The integral shuffle prism proving additivity of a bar insertion

  1. theorem OAI.PolycyclicRecognition.listBarTail_pair line 11
  2. theorem OAI.PolycyclicRecognition.listBarHeadMultiply_pair line 27
  3. theorem OAI.PolycyclicRecognition.listBarBoundary_pair_step line 46
  4. theorem OAI.PolycyclicRecognition.listBarBoundary_pair line 62