OAI/Algebra/AuslanderReiten/Tensor/ExternalTensorCubicExt.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.ExternalTensor.firstComparison line 22
2. def OAI.ArExplicit.ExternalTensor.secondComparison line 26
3. theorem OAI.ArExplicit.ExternalTensor.firstComparison_comm line 36
4. theorem OAI.ArExplicit.ExternalTensor.secondComparison_comm line 44
5. def OAI.ArExplicit.ExternalTensor.firstCubicExt line 49
6. def OAI.ArExplicit.ExternalTensor.secondCubicExt line 54
7. theorem OAI.ArExplicit.ExternalTensor.firstCubicExt_action line 60
8. theorem OAI.ArExplicit.ExternalTensor.secondCubicExt_action line 72