OAI/Algebra/AuslanderReiten/Tensor/BalancedTensorCategory.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.BalancedTensor.mapLeftLinear line 25
2. theorem OAI.ArExplicit.BalancedTensor.mapLeftLinear_tmul line 35
3. def OAI.ArExplicit.BalancedTensor.functor line 39
4. instance OAI.ArExplicit.BalancedTensor.(instance at line 45) line 45
5. def OAI.ArExplicit.BalancedTensor.naturalMap line 48
6. def OAI.ArExplicit.BalancedTensor.complexMap line 59
7. def OAI.ArExplicit.BalancedTensor.complexSequence line 66
8. theorem OAI.ArExplicit.BalancedTensor.complexSequence_shortExact line 78