OAI/Algebra/AuslanderReiten/Resolutions/BinaryKoszulDual.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.BinaryKoszul.DualPiece line 11
2. def OAI.ArExplicit.BinaryKoszul.dualRow line 13
3. def OAI.ArExplicit.BinaryKoszul.dualColumn line 16
4. theorem OAI.ArExplicit.BinaryKoszul.dualRow_apply line 21
5. theorem OAI.ArExplicit.BinaryKoszul.dualColumn_apply line 25
6. theorem OAI.ArExplicit.BinaryKoszul.exact_dual line 28
7. theorem OAI.ArExplicit.BinaryKoszul.dualRow_dualColumn line 36
8. theorem OAI.ArExplicit.BinaryKoszul.dualRow_surjective line 46
9. theorem OAI.ArExplicit.BinaryKoszul.dualColumn_injective line 53
10. theorem OAI.ArExplicit.BinaryKoszul.range_dualColumn_eq_ker_dualRow line 66
11. theorem OAI.ArExplicit.BinaryKoszul.dualColumn_zero_surjective line 94
12. def OAI.ArExplicit.BinaryKoszul.dualColumnZeroEquiv line 108