OAI/Algebra/AuslanderReiten/Tensor/BalancedTensorResolution.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- abbrev
OAI.ArExplicit.BalancedTensor.completeTensorline 21 - def
OAI.ArExplicit.BalancedTensor.tensorCokernelEquivline 25 - theorem
OAI.ArExplicit.BalancedTensor.tensorCokernelEquiv_mkline 31 - theorem
OAI.ArExplicit.BalancedTensor.completeTensor_totallyAcyclicline 38 - def
OAI.ArExplicit.BalancedTensor.completeTensorIsoline 43 - theorem
OAI.ArExplicit.BalancedTensor.tensorCokernelEquiv_naturalline 58 - theorem
OAI.ArExplicit.BalancedTensor.completeTensorIso_naturalline 79