OAI/Algebra/AuslanderReiten/Ext/TExtRecurrence.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.Resolution.tConnecting line 16
2. theorem OAI.ArExplicit.Resolution.tInducedDerived_shift_hom_zero line 21
3. theorem OAI.ArExplicit.Resolution.tSimpleDerived_negative_zero line 30
4. theorem OAI.ArExplicit.Resolution.tConnecting_multiply_bijective line 40
5. theorem OAI.ArExplicit.Resolution.tConnecting_multiply_surjective line 49
6. theorem OAI.ArExplicit.Resolution.tSimpleDerived_low_zero line 65
7. abbrev OAI.ArExplicit.Resolution.TSelfExt line 78
8. def OAI.ArExplicit.Resolution.tTau line 80
9. theorem OAI.ArExplicit.Resolution.tTau_hom line 83
10. theorem OAI.ArExplicit.Resolution.tTau_multiply_bijective line 87
11. theorem OAI.ArExplicit.Resolution.tSelfExt_low_zero line 110