OAI/Algebra/AuslanderReiten/Tensor/BalancedTensorFirst.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.BalancedTensor.mapFirst line 16
2. theorem OAI.ArExplicit.BalancedTensor.mapFirst_tmul line 22
3. theorem OAI.ArExplicit.BalancedTensor.mapFirst_id line 26
4. theorem OAI.ArExplicit.BalancedTensor.mapFirst_comp line 35
5. theorem OAI.ArExplicit.BalancedTensor.mapFirst_add line 45
6. theorem OAI.ArExplicit.BalancedTensor.mapFirst_zero line 55
7. theorem OAI.ArExplicit.BalancedTensor.exists_splitting line 63
8. theorem OAI.ArExplicit.BalancedTensor.mapFirst_shortExact line 104