OAI/Algebra/AuslanderReiten/Tensor/ExternalTensorModule.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArExplicit.ExternalTensor.left line 18
  2. def OAI.ArExplicit.ExternalTensor.right line 21
  3. theorem OAI.ArExplicit.ExternalTensor.left_tmul line 24
  4. theorem OAI.ArExplicit.ExternalTensor.right_tmul line 27
  5. theorem OAI.ArExplicit.ExternalTensor.left_right line 30
  6. def OAI.ArExplicit.ExternalTensor.representation line 37
  7. def OAI.ArExplicit.ExternalTensor.module line 42
  8. def OAI.ArExplicit.ExternalTensor.moduleObject line 45
  9. instance OAI.ArExplicit.ExternalTensor.baseModule line 49
  10. instance OAI.ArExplicit.ExternalTensor.tower line 52
  11. theorem OAI.ArExplicit.ExternalTensor.smul_tmul line 58
  12. instance OAI.ArExplicit.ExternalTensor.finite line 63
  13. def OAI.ArExplicit.ExternalTensor.map line 72
  14. theorem OAI.ArExplicit.ExternalTensor.map_tmul line 88