OAI/GroupTheory/PolycyclicRecognition/Algebra/TupleBarExteriorProduct.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The integral exterior product in abelian group homology

  1. def OAI.PolycyclicRecognition.tupleBarAdditiveClass line 13
  2. theorem OAI.PolycyclicRecognition.tupleBarAdditiveClass_update_add line 17
  3. def OAI.PolycyclicRecognition.tupleBarClassCoordinate line 30
  4. def OAI.PolycyclicRecognition.tupleBarAlternating line 36
  5. def OAI.PolycyclicRecognition.tupleBarExteriorProduct line 49
  6. theorem OAI.PolycyclicRecognition.tupleBarExteriorProduct_value line 54