OAI/Algebra/AuslanderReiten/Ext/TExtPolynomial.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.Resolution.tTauMul line 18
2. def OAI.ArExplicit.Resolution.tTauMulEquiv line 21
3. def OAI.ArExplicit.Resolution.tExtCoefficientEquiv line 24
4. def OAI.ArExplicit.Resolution.tTauPower line 28
5. theorem OAI.ArExplicit.Resolution.tTauPower_zero line 30
6. theorem OAI.ArExplicit.Resolution.tTauPower_succ line 33
7. theorem OAI.ArExplicit.Resolution.tTauPower_ne_zero line 37
8. theorem OAI.ArExplicit.Resolution.tSelfExt_coefficient line 43
9. theorem OAI.ArExplicit.Resolution.tSelfExt_zero_of_not_dvd line 55
10. theorem OAI.ArExplicit.Resolution.tTauPower_mul_aux line 68
11. theorem OAI.ArExplicit.Resolution.tTauPower_mul line 83