OAI/Analysis/Pureness/Tensor/SpatialRepresentationIndependence.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.spatialTensorSwap line 12
2. lemma OAI.CuntzPureness.spatialTensorSwap_tmul line 22
3. lemma OAI.CuntzPureness.spatialTensorSwap_op line 27
4. lemma OAI.CuntzPureness.spatialStarTensor_swap line 39
5. lemma OAI.CuntzPureness.spatialStarTensor_norm_le_swap line 48
6. theorem OAI.CuntzPureness.spatialStarTensor_norm_swap line 58
7. theorem OAI.CuntzPureness.spatialStarTensor_norm_representation_independent line 69
8. theorem OAI.CuntzPureness.spatialStarTensor_norm_le_faithful line 80