OAI/Algebra/AuslanderReiten/Algebras/TMultiplication.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ArExplicit.Letter.sum_univ line 11
  2. def OAI.ArExplicit.CocycleData.multiplicationCoefficient line 25
  3. theorem OAI.ArExplicit.CocycleData.dual_apply line 29
  4. theorem OAI.ArExplicit.CocycleData.upper_product_coefficient line 34
  5. theorem OAI.ArExplicit.CocycleData.multiplication_false_e line 41
  6. theorem OAI.ArExplicit.CocycleData.multiplication_false_x line 45
  7. theorem OAI.ArExplicit.CocycleData.multiplication_false_y line 50
  8. theorem OAI.ArExplicit.CocycleData.multiplication_false_z line 55
  9. theorem OAI.ArExplicit.CocycleData.multiplication_false_u line 60
  10. theorem OAI.ArExplicit.CocycleData.multiplication_false_v line 64
  11. theorem OAI.ArExplicit.CocycleData.multiplication_false_t line 69
  12. theorem OAI.ArExplicit.CocycleData.multiplication_false_j line 73
  13. theorem OAI.ArExplicit.CocycleData.multiplication_false_f line 78
  14. theorem OAI.ArExplicit.CocycleData.multiplication_false_n line 82
  15. theorem OAI.ArExplicit.CocycleData.multiplication_true_e line 87
  16. theorem OAI.ArExplicit.CocycleData.multiplication_true_x line 93
  17. theorem OAI.ArExplicit.CocycleData.multiplication_true_y line 99
  18. theorem OAI.ArExplicit.CocycleData.multiplication_true_z line 105
  19. theorem OAI.ArExplicit.CocycleData.multiplication_true_u line 111
  20. theorem OAI.ArExplicit.CocycleData.multiplication_true_v line 117
  21. theorem OAI.ArExplicit.CocycleData.multiplication_true_t line 123
  22. theorem OAI.ArExplicit.CocycleData.multiplication_true_j line 129
  23. theorem OAI.ArExplicit.CocycleData.multiplication_true_f line 135
  24. theorem OAI.ArExplicit.CocycleData.multiplication_true_n line 141
  25. theorem OAI.ArExplicit.CocycleData.multiplication_coefficient line 147