OAI/Algebra/AuslanderReiten/Ext/TTensorActions.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.ExternalTensor.diagonalFirst_injective line 15
2. theorem OAI.ArExplicit.ExternalTensor.diagonalSecond_injective line 24
3. theorem OAI.ArExplicit.ExternalTensor.coefficientFirst_apply line 33
4. theorem OAI.ArExplicit.ExternalTensor.coefficientSecond_apply line 49
5. theorem OAI.ArExplicit.ExternalTensor.coefficientFirst_zero line 65
6. theorem OAI.ArExplicit.ExternalTensor.coefficientSecond_zero line 79
7. def OAI.ArExplicit.Resolution.tTensorScalarEquiv line 103
8. theorem OAI.ArExplicit.Resolution.tTensorScalarEquiv_tmul line 109
9. theorem OAI.ArExplicit.Resolution.tExplicitCoefficientEquiv_succ line 114
10. theorem OAI.ArExplicit.Resolution.tTensorScalarEquiv_first line 121
11. theorem OAI.ArExplicit.Resolution.tTensorScalarEquiv_second line 133
12. def OAI.ArExplicit.Resolution.tTensorScalarAt line 145
13. theorem OAI.ArExplicit.Resolution.tTensorScalarAt_congr line 148
14. theorem OAI.ArExplicit.Resolution.tTensorCoefficientEquiv_apply line 156
15. theorem OAI.ArExplicit.Resolution.polynomialDiagonal_succ line 160
16. theorem OAI.ArExplicit.Resolution.polynomialDiagonal_castSucc line 166
17. theorem OAI.ArExplicit.Resolution.tTensorCoefficient_first line 176
18. theorem OAI.ArExplicit.Resolution.tTensorCoefficient_second line 198