OAI/Algebra/AuslanderReiten/Tensor/ExternalTensorHomCubic.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.ExternalTensor.elementary_cubicInsert_same line 18
2. theorem OAI.ArExplicit.ExternalTensor.elementary_cubicInsert_ne line 27
3. theorem OAI.ArExplicit.ExternalTensor.map_first_comp line 37
4. theorem OAI.ArExplicit.ExternalTensor.elementary_firstCubic line 53
5. theorem OAI.ArExplicit.ExternalTensor.map_second_comp line 84
6. theorem OAI.ArExplicit.ExternalTensor.elementary_secondCubic line 100