OAI/GroupTheory/PolycyclicRecognition/Algebra/TupleBarProductPrism.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Additivity of the higher integral bar class in every coordinate

  1. def OAI.PolycyclicRecognition.tupleBarProductPrism line 15
  2. theorem OAI.PolycyclicRecognition.tupleBarProductPrism_toList line 27
  3. theorem OAI.PolycyclicRecognition.tupleBarProductPrism_boundary line 33
  4. theorem OAI.PolycyclicRecognition.tupleBarProductClass_update_mul line 44