OAI/Algebra/AuslanderReiten/Duality/DualTensorModule.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.ArExplicit.DualTensor.moduleEvaluationline 12 - theorem
OAI.ArExplicit.DualTensor.moduleEvaluation_tmulline 21 - def
OAI.ArExplicit.DualTensor.moduleEvaluationEquivline 24 - def
OAI.ArExplicit.DualTensor.precomposeRightline 29 - theorem
OAI.ArExplicit.DualTensor.moduleEvaluation_naturalline 34