OAI/Algebra/AuslanderReiten/Tensor/ExternalEnveloping.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ArExplicit.ExternalTensor.ProductEnveloping line 18
2. abbrev OAI.ArExplicit.ExternalTensor.EnvelopingProduct line 19
3. def OAI.ArExplicit.ExternalTensor.envelopingEquiv line 21
4. theorem OAI.ArExplicit.ExternalTensor.envelopingEquiv_tmul line 26
5. theorem OAI.ArExplicit.ExternalTensor.envelopingEquiv_symm_tmul line 31
6. abbrev OAI.ArExplicit.ExternalTensor.envelopingFunctor line 37
7. abbrev OAI.ArExplicit.ExternalTensor.envelopingObject line 41
8. instance OAI.ArExplicit.ExternalTensor.forwardInverse line 44
9. instance OAI.ArExplicit.ExternalTensor.backwardInverse line 49
10. def OAI.ArExplicit.ExternalTensor.envelopingSemilinear line 54
11. theorem OAI.ArExplicit.ExternalTensor.enveloping_projective line 66
12. instance OAI.ArExplicit.ExternalTensor.envelopingBaseModule line 71
13. instance OAI.ArExplicit.ExternalTensor.envelopingTower line 74
14. instance OAI.ArExplicit.ExternalTensor.envelopingFinite line 82