OAI/Algebra/AuslanderReiten/Tensor/BalancedTensorExact.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ArExplicit.BalancedTensor.rightCoefficientsline 22 - theorem
OAI.ArExplicit.BalancedTensor.rightCoefficients_tmulline 46 - def
OAI.ArExplicit.BalancedTensor.freeRecombineline 50 - theorem
OAI.ArExplicit.BalancedTensor.freeRecombine_applyline 56 - theorem
OAI.ArExplicit.BalancedTensor.freeRecombine_rightCoefficientsline 61 - theorem
OAI.ArExplicit.BalancedTensor.rightCoefficients_naturalline 94 - theorem
OAI.ArExplicit.BalancedTensor.freeRecombine_naturalline 106 - theorem
OAI.ArExplicit.BalancedTensor.mapRight_exactline 112