OAI/Analysis/Pureness/Tensor/SpatialTensorQuotient.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.CuntzPureness.spatialTensorQuotientMap line 18
2. lemma OAI.CuntzPureness.spatialTensorQuotientMap_tensor line 22
3. lemma OAI.CuntzPureness.spatialTensorQuotientMap_surjective line 27
4. lemma OAI.CuntzPureness.spatialTensorQuotientMap_ideal_zero line 32
5. abbrev OAI.CuntzPureness.SpatialTensorIdealQuotient line 38
6. instance OAI.CuntzPureness.spatialTensorIdealQuotientCStar line 40
7. def OAI.CuntzPureness.spatialTensorQuotientFactor line 45
8. lemma OAI.CuntzPureness.spatialTensorQuotientFactor_map line 51
9. lemma OAI.CuntzPureness.spatialTensorQuotientFactor_surjective line 56
10. lemma OAI.CuntzPureness.spatialTensorQuotientFactor_norm_le line 62
11. theorem OAI.CuntzPureness.spatialTensorQuotientFactor_injective_iff line 66