OAI/Algebra/AuslanderReiten/Tensor/ExternalTensorForget.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArExplicit.ExternalTensor.forgetField line 15
  2. abbrev OAI.ArExplicit.ExternalTensor.forgetComplex line 18
  3. instance OAI.ArExplicit.ExternalTensor.hasScalarTotal line 23
  4. abbrev OAI.ArExplicit.ExternalTensor.scalarTotal line 26
  5. abbrev OAI.ArExplicit.ExternalTensor.scalarSummands line 30
  6. def OAI.ArExplicit.ExternalTensor.scalarTermDirectSumEquiv line 33
  7. def OAI.ArExplicit.ExternalTensor.forgetTermEquiv line 37
  8. abbrev OAI.ArExplicit.ExternalTensor.scalarInclusion line 42
  9. def OAI.ArExplicit.ExternalTensor.forgetTermIso line 47
  10. theorem OAI.ArExplicit.ExternalTensor.scalarTermDirectSumEquiv_inclusion line 51
  11. theorem OAI.ArExplicit.ExternalTensor.scalarInclusion_forgetTermIso_inv line 59
  12. abbrev OAI.ArExplicit.ExternalTensor.scalarHorizontal line 74
  13. abbrev OAI.ArExplicit.ExternalTensor.scalarVertical line 78
  14. theorem OAI.ArExplicit.ExternalTensor.scalarHorizontal_comp line 82
  15. theorem OAI.ArExplicit.ExternalTensor.scalarVertical_comp line 106
  16. theorem OAI.ArExplicit.ExternalTensor.scalarInclusion_d line 130
  17. def OAI.ArExplicit.ExternalTensor.scalarForgetTotalIso line 136
  18. def OAI.ArExplicit.ExternalTensor.forgetTotalIso line 157
  19. theorem OAI.ArExplicit.ExternalTensor.scalarForgetTotalIso_naturality line 163