OAI/Algebra/AuslanderReiten/Ext/TExplicitPolynomial.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.Resolution.tPMul line 17
2. def OAI.ArExplicit.Resolution.tPMulEquiv line 20
3. def OAI.ArExplicit.Resolution.tExplicitCoefficientEquiv line 23
4. def OAI.ArExplicit.Resolution.tExplicitPower line 27
5. theorem OAI.ArExplicit.Resolution.tExplicitPower_zero line 29
6. theorem OAI.ArExplicit.Resolution.tExplicitPower_succ line 32
7. theorem OAI.ArExplicit.Resolution.tExplicitPower_ne_zero line 36
8. theorem OAI.ArExplicit.Resolution.tExplicit_coefficient line 42
9. theorem OAI.ArExplicit.Resolution.tExplicit_zero_of_not_dvd line 54
10. theorem OAI.ArExplicit.Resolution.tExplicitPower_mul_aux line 67
11. theorem OAI.ArExplicit.Resolution.tExplicitPower_mul line 82