OAI/Algebra/AuslanderReiten/Cocycles/CocycleCertificate.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.CocycleData.certificate line 8
  2. theorem OAI.ArExplicit.CocycleData.valid_false_e line 11
  3. theorem OAI.ArExplicit.CocycleData.valid_false_x line 13
  4. theorem OAI.ArExplicit.CocycleData.valid_false_y line 15
  5. theorem OAI.ArExplicit.CocycleData.valid_false_z line 17
  6. theorem OAI.ArExplicit.CocycleData.valid_false_u line 19
  7. theorem OAI.ArExplicit.CocycleData.valid_false_v line 21
  8. theorem OAI.ArExplicit.CocycleData.valid_false_t line 23
  9. theorem OAI.ArExplicit.CocycleData.valid_false_j line 25
  10. theorem OAI.ArExplicit.CocycleData.valid_false_f line 27
  11. theorem OAI.ArExplicit.CocycleData.valid_false_n line 29
  12. theorem OAI.ArExplicit.CocycleData.valid_true_e line 31
  13. theorem OAI.ArExplicit.CocycleData.valid_true_x line 33
  14. theorem OAI.ArExplicit.CocycleData.valid_true_y line 35
  15. theorem OAI.ArExplicit.CocycleData.valid_true_z line 37
  16. theorem OAI.ArExplicit.CocycleData.valid_true_u line 39
  17. theorem OAI.ArExplicit.CocycleData.valid_true_v line 41
  18. theorem OAI.ArExplicit.CocycleData.valid_true_t line 43
  19. theorem OAI.ArExplicit.CocycleData.valid_true_j line 45
  20. theorem OAI.ArExplicit.CocycleData.valid_true_f line 47
  21. theorem OAI.ArExplicit.CocycleData.valid_true_n line 49
  22. theorem OAI.ArExplicit.CocycleData.certificate_valid line 51
  23. theorem OAI.ArExplicit.CocycleData.differentialBlock_sum_zero line 75
  24. theorem OAI.ArExplicit.CocycleData.sum_partition line 80
  25. theorem OAI.ArExplicit.CocycleData.differentialTerms_sum_zero line 93