OAI/Algebra/AuslanderReiten/Tensor/BalancedTensorEquiv.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ArExplicit.BalancedTensor.inverse_equivariant_right line 19
2. theorem OAI.ArExplicit.BalancedTensor.inverse_equivariant_left line 25
3. def OAI.ArExplicit.BalancedTensor.congr line 30
4. theorem OAI.ArExplicit.BalancedTensor.congr_tmul line 53
5. theorem OAI.ArExplicit.BalancedTensor.congr_smul line 63
6. def OAI.ArExplicit.BalancedTensor.congrLeft line 70