OAI/Algebra/AuslanderReiten/Ext/ExceptionalExt.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.Resolution.dualHom_exceptional_decomposition line 19
2. theorem OAI.ArExplicit.Resolution.extMk_smul_regular line 41
3. def OAI.ArExplicit.Resolution.exceptionalExtLinear line 54
4. theorem OAI.ArExplicit.Resolution.exceptionalExtLinear_injective line 58
5. theorem OAI.ArExplicit.Resolution.regular_ext_two_representative line 66
6. theorem OAI.ArExplicit.Resolution.exceptionalExtLinear_surjective line 106
7. def OAI.ArExplicit.Resolution.exceptionalExtEquiv line 112
8. theorem OAI.ArExplicit.Resolution.regular_ext_two_finrank line 117
9. theorem OAI.ArExplicit.Resolution.regular_ext_two_right_action line 122
10. theorem OAI.ArExplicit.Resolution.exceptionalExtEquiv_right_action line 144