OAI/Algebra/AuslanderReiten/Tensor/ExternalTensorCubic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.ExternalTensor.cubicInsert line 18
2. def OAI.ArExplicit.ExternalTensor.firstCubicEntry line 26
3. def OAI.ArExplicit.ExternalTensor.secondCubicEntry line 34
4. def OAI.ArExplicit.ExternalTensor.firstCubic line 42
5. def OAI.ArExplicit.ExternalTensor.secondCubic line 46
6. theorem OAI.ArExplicit.ExternalTensor.firstCubic_insert line 50
7. theorem OAI.ArExplicit.ExternalTensor.secondCubic_insert line 56