OAI/Algebra/AuslanderReiten/Ext/AExtActions.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.Resolution.aFactorResolution line 21
2. abbrev OAI.ArExplicit.Resolution.aFactorCubic line 25
3. abbrev OAI.ArExplicit.Resolution.aFactorCubic_comm line 26
4. theorem OAI.ArExplicit.Resolution.aFactorExtClass line 31
5. abbrev OAI.ArExplicit.Resolution.aCanonicalFirst line 35
6. abbrev OAI.ArExplicit.Resolution.aCanonicalSecond line 39
7. abbrev OAI.ArExplicit.Resolution.aFirst line 43
8. abbrev OAI.ArExplicit.Resolution.aSecond line 47
9. theorem OAI.ArExplicit.Resolution.aFactorCubic_class line 52
10. theorem OAI.ArExplicit.Resolution.aCanonicalFirst_action line 59
11. theorem OAI.ArExplicit.Resolution.aCanonicalSecond_action line 71
12. theorem OAI.ArExplicit.Resolution.aFirst_kunneth line 83
13. theorem OAI.ArExplicit.Resolution.aSecond_kunneth line 89