OAI/Analysis/Quantum/DimensionTen/Kraus.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DimensionTen.krausMap line 11
2. lemma OAI.DimensionTen.krausMap_add line 15
3. lemma OAI.DimensionTen.krausMap_smul line 20
4. lemma OAI.DimensionTen.krausMap_linear line 25
5. lemma OAI.DimensionTen.posSemidef_sum line 29
6. lemma OAI.DimensionTen.krausMap_positive line 39
7. lemma OAI.DimensionTen.krausMap_entry line 44
8. lemma OAI.DimensionTen.amplify_kraus line 53
9. lemma OAI.DimensionTen.krausMap_cp line 68
10. lemma OAI.DimensionTen.krausMap_single line 74
11. lemma OAI.DimensionTen.krausMap_adjoint line 79