OAI/GroupTheory/PolycyclicRecognition/Algebra/ExteriorSquarePairing.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The alternating exterior-square pairing used on abelian bar cycles

  1. def OAI.PolycyclicRecognition.exteriorSquareValue line 12
  2. theorem OAI.PolycyclicRecognition.exteriorSquareValue_swap line 15
  3. theorem OAI.PolycyclicRecognition.exteriorSquareValue_add_left line 25
  4. theorem OAI.PolycyclicRecognition.exteriorSquareValue_add_right line 29
  5. theorem OAI.PolycyclicRecognition.exteriorSquareValue_zero_left line 35
  6. theorem OAI.PolycyclicRecognition.exteriorSquareValue_zero_right line 38
  7. def OAI.PolycyclicRecognition.exteriorSquarePairing line 41
  8. theorem OAI.PolycyclicRecognition.exteriorSquarePairing_apply line 55