OAI/Analysis/Quantum/DimensionTen/ExteriorMaps.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DimensionTen.exteriorKraus line 13
  2. lemma OAI.DimensionTen.exteriorMap_kraus line 16
  3. lemma OAI.DimensionTen.exteriorMap_output_transpose line 25
  4. lemma OAI.DimensionTen.exteriorMap_input_transpose line 30
  5. def OAI.DimensionTen.complementaryKraus line 35
  6. lemma OAI.DimensionTen.complementaryMap_kraus line 38
  7. lemma OAI.DimensionTen.complementaryMap_input_transpose line 44
  8. lemma OAI.DimensionTen.complementaryMap_output_transpose line 47
  9. def OAI.DimensionTen.phiOneKraus line 51
  10. def OAI.DimensionTen.phiTwoKraus line 53
  11. lemma OAI.DimensionTen.phiOne_kraus line 55
  12. lemma OAI.DimensionTen.phiTwo_kraus line 61
  13. lemma OAI.DimensionTen.phiOne_output_transpose line 69
  14. lemma OAI.DimensionTen.phiTwo_output_transpose line 73
  15. lemma OAI.DimensionTen.phiOne_ppt line 76
  16. lemma OAI.DimensionTen.phiTwo_ppt line 83