OAI/Algebra/AuslanderReiten/Tensor/BalancedTensorCompleteAction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ArExplicit.BalancedTensor.nativeEvaluationIso line 29
2. def OAI.ArExplicit.BalancedTensor.completeActionEndpoint line 33
3. def OAI.ArExplicit.BalancedTensor.completeActionCokernelIso line 40
4. def OAI.ArExplicit.BalancedTensor.completeActionIn line 48
5. def OAI.ArExplicit.BalancedTensor.completeActionOut line 53
6. theorem OAI.ArExplicit.BalancedTensor.completeAction_inverse line 59
7. theorem OAI.ArExplicit.BalancedTensor.completeAction_inverse' line 68
8. theorem OAI.ArExplicit.BalancedTensor.completeAction_scalar line 75
9. theorem OAI.ArExplicit.BalancedTensor.completeActionCokernelIso_eq line 94
10. theorem OAI.ArExplicit.BalancedTensor.completeActionOut_quotient line 108