OAI/Algebra/AuslanderReiten/Cocycles/CocycleCorners.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.TIndex.lowerSource line 10
  2. def OAI.ArExplicit.TIndex.lowerTarget line 14
  3. def OAI.ArExplicit.TIndex.source line 18
  4. def OAI.ArExplicit.TIndex.target line 19
  5. def OAI.ArExplicit.TIndex.vertex line 21
  6. def OAI.ArExplicit.TIndex.weight line 23
  7. theorem OAI.ArExplicit.CocycleData.cochain_data_properties line 29
  8. theorem OAI.ArExplicit.CocycleData.cochain_term_properties line 36
  9. theorem OAI.ArExplicit.CocycleData.coefficient_mul_vertex line 45
  10. theorem OAI.ArExplicit.CocycleData.coefficient_vertex_mul line 54
  11. theorem OAI.ArExplicit.CocycleData.p_normalized_first line 63
  12. theorem OAI.ArExplicit.CocycleData.p_normalized_second line 74
  13. theorem OAI.ArExplicit.CocycleData.p_normalized_third line 85
  14. theorem OAI.ArExplicit.CocycleData.p_balanced_first line 96
  15. theorem OAI.ArExplicit.CocycleData.p_balanced_second line 107
  16. theorem OAI.ArExplicit.CocycleData.vertex_mul_vector line 118
  17. theorem OAI.ArExplicit.CocycleData.vector_mul_vertex line 126
  18. theorem OAI.ArExplicit.CocycleData.p_left_vertex line 134
  19. theorem OAI.ArExplicit.CocycleData.p_right_vertex line 148