OAI/Algebra/AuslanderReiten/Tensor/ExternalTensorFunctor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.ExternalTensor.mapHom line 19
2. theorem OAI.ArExplicit.ExternalTensor.mapHom_id line 25
3. theorem OAI.ArExplicit.ExternalTensor.mapHom_comp line 34
4. theorem OAI.ArExplicit.ExternalTensor.mapHom_add_left line 49
5. theorem OAI.ArExplicit.ExternalTensor.mapHom_add_right line 63
6. def OAI.ArExplicit.ExternalTensor.rightFunctor line 77
7. instance OAI.ArExplicit.ExternalTensor.(instance at line 83) line 83
8. def OAI.ArExplicit.ExternalTensor.bifunctor line 86
9. instance OAI.ArExplicit.ExternalTensor.(instance at line 104) line 104
10. instance OAI.ArExplicit.ExternalTensor.(instance at line 111) line 111