OAI/Algebra/AuslanderReiten/Resolutions/BinaryKoszul.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArExplicit.BinaryKoszul.Piece line 13
  2. theorem OAI.ArExplicit.BinaryKoszul.cons_succ_castSucc line 17
  3. theorem OAI.ArExplicit.BinaryKoszul.snoc_castSucc_succ line 24
  4. def OAI.ArExplicit.BinaryKoszul.mulX line 28
  5. def OAI.ArExplicit.BinaryKoszul.mulY line 33
  6. theorem OAI.ArExplicit.BinaryKoszul.mulX_zero line 39
  7. theorem OAI.ArExplicit.BinaryKoszul.mulX_succ line 41
  8. theorem OAI.ArExplicit.BinaryKoszul.mulY_last line 44
  9. theorem OAI.ArExplicit.BinaryKoszul.mulY_castSucc line 47
  10. theorem OAI.ArExplicit.BinaryKoszul.mulX_injective line 50
  11. theorem OAI.ArExplicit.BinaryKoszul.mulY_injective line 55
  12. theorem OAI.ArExplicit.BinaryKoszul.mul_commute line 61
  13. def OAI.ArExplicit.BinaryKoszul.row line 67
  14. def OAI.ArExplicit.BinaryKoszul.column line 70
  15. theorem OAI.ArExplicit.BinaryKoszul.row_apply line 74
  16. theorem OAI.ArExplicit.BinaryKoszul.column_apply line 77
  17. theorem OAI.ArExplicit.BinaryKoszul.row_column line 80
  18. theorem OAI.ArExplicit.BinaryKoszul.column_injective line 87
  19. theorem OAI.ArExplicit.BinaryKoszul.kernel_row line 92
  20. theorem OAI.ArExplicit.BinaryKoszul.range_column_eq_ker_row line 115
  21. theorem OAI.ArExplicit.BinaryKoszul.row_surjective line 122
  22. theorem OAI.ArExplicit.BinaryKoszul.row_zero_injective line 134
  23. def OAI.ArExplicit.BinaryKoszul.rowZeroEquiv line 151