OAI/Analysis/TracialSplitting/SpatialTensor.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UnitalTomsWinter.SpatialHilbert line 37
  2. def OAI.UnitalTomsWinter.spatialTensorOp line 41
  3. lemma OAI.UnitalTomsWinter.spatialTensorOp_coe line 45
  4. lemma OAI.UnitalTomsWinter.spatialTensorOp_ext line 49
  5. lemma OAI.UnitalTomsWinter.spatialTensorOp_zero_left line 60
  6. lemma OAI.UnitalTomsWinter.spatialTensorOp_zero_right line 63
  7. lemma OAI.UnitalTomsWinter.spatialTensorOp_add_left line 66
  8. lemma OAI.UnitalTomsWinter.spatialTensorOp_add_right line 70
  9. lemma OAI.UnitalTomsWinter.spatialTensorOp_smul_left line 74
  10. lemma OAI.UnitalTomsWinter.spatialTensorOp_smul_right line 79
  11. lemma OAI.UnitalTomsWinter.spatialTensorOp_mul line 83
  12. lemma OAI.UnitalTomsWinter.completion_opNorm_le line 87
  13. lemma OAI.UnitalTomsWinter.spatialTensorOp_norm_le line 95
  14. lemma OAI.UnitalTomsWinter.spatialTensorOp_star line 101
  15. lemma OAI.Pureness.spatialTensorOp_one line 134
  16. def OAI.Pureness.spatialLeftHom line 139
  17. def OAI.Pureness.spatialRightHom line 150
  18. lemma OAI.Pureness.spatialLeftRight_commute line 161
  19. lemma OAI.Pureness.spatialRightHom_injective line 168
  20. def OAI.Pureness.spatialStarTensorHom line 182
  21. lemma OAI.Pureness.spatialStarTensorHom_tmul line 186
  22. lemma OAI.Pureness.spatial_relation_coefficients_zero line 209
  23. theorem OAI.Pureness.spatialStarTensorHom_injective_of_faithful line 238