OAI/Algebra/AuslanderReiten/Ext/BaseExt.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.Resolution.dualHom_exact_one line 17
2. theorem OAI.ArExplicit.Resolution.dualHom_exact_tail line 28
3. theorem OAI.ArExplicit.Resolution.hom_simple_regular_eq_zero line 43
4. theorem OAI.ArExplicit.Resolution.regular_ext_zero line 60
5. theorem OAI.ArExplicit.Resolution.regular_ext_one line 68
6. theorem OAI.ArExplicit.Resolution.regular_ext_tail line 85
7. theorem OAI.ArExplicit.Resolution.regular_ext_vanish line 108
8. def OAI.ArExplicit.Resolution.exceptionalHom line 117
9. theorem OAI.ArExplicit.Resolution.exceptionalHom_cocycle line 120
10. theorem OAI.ArExplicit.Resolution.exceptionalHom_not_boundary line 126
11. def OAI.ArExplicit.Resolution.regular_ext_two_class line 134
12. theorem OAI.ArExplicit.Resolution.regular_ext_two_class_ne_zero line 141