OAI/Analysis/Quantum/PPTSquare/TensorModel.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TensorCriterion.product line 14
  2. def OAI.TensorCriterion.projector line 17
  3. def OAI.TensorCriterion.hsAdjoint line 19
  4. def OAI.TensorCriterion.tensorMap line 33
  5. def OAI.TensorCriterion.symPair line 60
  6. def OAI.TensorCriterion.altPair line 63
  7. def OAI.TensorCriterion.rt line 65
  8. def OAI.TensorCriterion.U line 67
  9. def OAI.TensorCriterion.V line 72
  10. def OAI.TensorCriterion.complement line 75
  11. def OAI.TensorCriterion.complementSign line 76
  12. def OAI.TensorCriterion.K line 77
  13. def OAI.TensorCriterion.E line 79
  14. def OAI.TensorCriterion.S line 81
  15. def OAI.TensorCriterion.R line 83
  16. def OAI.TensorCriterion.Phi1 line 86
  17. def OAI.TensorCriterion.Phi2 line 88
  18. def OAI.TensorCriterion.Z line 90
  19. def OAI.TensorCriterion.DistinctDirections line 93
  20. def OAI.TensorCriterion.QuadraticEvaluations line 96
  21. lemma OAI.TensorCriterion.rt_star line 107
  22. lemma OAI.TensorCriterion.rt_ne line 108
  23. lemma OAI.TensorCriterion.rt_sq line 111
  24. lemma OAI.TensorCriterion.inv_rt_sq line 114
  25. def OAI.TensorCriterion.compound line 118
  26. lemma OAI.TensorCriterion.V_compression line 122
  27. lemma OAI.TensorCriterion.complement_involution line 135
  28. lemma OAI.TensorCriterion.complement_sign line 137
  29. lemma OAI.TensorCriterion.complement_sign_star line 139
  30. lemma OAI.TensorCriterion.K_hermitian line 142
  31. lemma OAI.TensorCriterion.K_mul line 155
  32. lemma OAI.TensorCriterion.mul_K line 160
  33. lemma OAI.TensorCriterion.exterior_dual_apply line 165
  34. lemma OAI.TensorCriterion.compound_pair_diagonal line 172
  35. lemma OAI.TensorCriterion.compound_pair_trace line 180