OAI/Algebra/AuslanderReiten/Ext/TTensorPolynomial.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.Resolution.tTensorCoefficients line 17
2. def OAI.ArExplicit.Resolution.polynomialDiagonal line 22
3. theorem OAI.ArExplicit.Resolution.polynomialDiagonal_injective line 25
4. theorem OAI.ArExplicit.Resolution.polynomialDiagonal_hits line 33
5. theorem OAI.ArExplicit.Resolution.tensor_zero_left line 48
6. theorem OAI.ArExplicit.Resolution.tensor_zero_right line 55
7. theorem OAI.ArExplicit.Resolution.tTensorCoefficient_off_diagonal line 63
8. def OAI.ArExplicit.Resolution.tTensorCoefficientEquiv line 71
9. theorem OAI.ArExplicit.Resolution.tTensorCoefficient_zero_of_not_dvd line 79