OAI/Algebra/AuslanderReiten/Ext/TensorExtCoefficients.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.ExternalTensor.extCoefficients line 14
2. abbrev OAI.ArExplicit.ExternalTensor.diagonalFirst line 17
3. abbrev OAI.ArExplicit.ExternalTensor.diagonalSecond line 20
4. def OAI.ArExplicit.ExternalTensor.coefficientFirst line 25
5. def OAI.ArExplicit.ExternalTensor.coefficientSecond line 34
6. theorem OAI.ArExplicit.ExternalTensor.coefficientFirst_single line 43
7. theorem OAI.ArExplicit.ExternalTensor.coefficientSecond_single line 57