OAI/Algebra/AuslanderReiten/Cocycles/CocycleFormula.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.CocycleData.evalQuad line 14
2. theorem OAI.ArExplicit.CocycleData.list_mul_sum line 18
3. theorem OAI.ArExplicit.CocycleData.list_sum_mul line 24
4. theorem OAI.ArExplicit.CocycleData.list_sum_map_add line 30

   Also declared: OAI/Algebra/AuslanderReiten/Cocycles/TwistedBoundaryFormula.lean:24 (same declaration text).

5. theorem OAI.ArExplicit.CocycleData.list_sum_flatMap line 37

   Also declared: OAI/Algebra/AuslanderReiten/Cocycles/TwistedBoundaryFormula.lean:17 (same declaration text).

6. theorem OAI.ArExplicit.CocycleData.row_differential line 44
7. theorem OAI.ArExplicit.CocycleData.list_left_mul line 62
8. theorem OAI.ArExplicit.CocycleData.list_right_mul line 68

   Also declared: OAI/Algebra/AuslanderReiten/Cocycles/TwistedBoundaryFormula.lean:31 (same declaration text).

9. theorem OAI.ArExplicit.CocycleData.p_differential_formula line 74