OAI/Algebra/AuslanderReiten/Tensor/ExternalTensorComplex.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.ArExplicit.ExternalTensor.hasTotal line 24
2. abbrev OAI.ArExplicit.ExternalTensor.complex line 27
3. abbrev OAI.ArExplicit.ExternalTensor.Diagonal line 30
4. instance OAI.ArExplicit.ExternalTensor.(instance at line 32) line 32
5. abbrev OAI.ArExplicit.ExternalTensor.summands line 35
6. def OAI.ArExplicit.ExternalTensor.termDirectSumEquiv line 38
7. def OAI.ArExplicit.ExternalTensor.termPiEquiv line 42
8. theorem OAI.ArExplicit.ExternalTensor.term_finite line 49
9. theorem OAI.ArExplicit.ExternalTensor.term_projective line 59