OAI/Analysis/Pureness/Tensor/SpatialCommutingTensor.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CuntzPureness.spatialTensorOp_one line 15
  2. def OAI.CuntzPureness.spatialLeftHom line 20
  3. def OAI.CuntzPureness.spatialRightHom line 31
  4. lemma OAI.CuntzPureness.spatialLeftRight_commute line 42
  5. lemma OAI.CuntzPureness.spatialRightHom_injective line 49
  6. def OAI.CuntzPureness.spatialStarTensorHom line 63
  7. lemma OAI.CuntzPureness.spatialStarTensorHom_tmul line 67
  8. lemma OAI.CuntzPureness.spatialStarTensorHom_injective line 72
  9. abbrev OAI.CuntzPureness.representedSpatialTensor line 79
  10. lemma OAI.CuntzPureness.representedSpatialTensor_dense line 82