OAI/Analysis/Quantum/DimensionTen/PureMatrices.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DimensionTen.pure line 11
  2. lemma OAI.DimensionTen.pure_posSemidef line 13
  3. lemma OAI.DimensionTen.pure_conjugate line 16
  4. lemma OAI.DimensionTen.pure_kronecker line 20
  5. lemma OAI.DimensionTen.trace_pure_mul line 26
  6. lemma OAI.DimensionTen.product_dot line 31
  7. def OAI.DimensionTen.omega line 43
  8. lemma OAI.DimensionTen.choi_eq_amplify line 45
  9. lemma OAI.DimensionTen.cp_choi_posSemidef line 54
  10. lemma OAI.DimensionTen.cp_comp line 59
  11. lemma OAI.DimensionTen.linear_comp line 65
  12. lemma OAI.DimensionTen.eb_choi_separable line 72