OAI/Analysis/Quantum/PPTSquare/SymmetricVectors.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TensorCriterion.symWeight line 13
  2. def OAI.TensorCriterion.xhat line 15
  3. lemma OAI.TensorCriterion.symWeight_ne line 18
  4. lemma OAI.TensorCriterion.U_xhat_row0 line 22
  5. lemma OAI.TensorCriterion.U_xhat_row1 line 28
  6. lemma OAI.TensorCriterion.U_xhat_row2 line 34
  7. lemma OAI.TensorCriterion.U_xhat_row3 line 40
  8. lemma OAI.TensorCriterion.U_xhat line 46
  9. lemma OAI.TensorCriterion.xhat_source line 54
  10. lemma OAI.TensorCriterion.ad_projector line 66
  11. lemma OAI.TensorCriterion.projector_product line 70
  12. lemma OAI.TensorCriterion.S_projector line 77
  13. lemma OAI.TensorCriterion.R_projector line 83
  14. lemma OAI.TensorCriterion.exterior_projector_pairing line 87
  15. lemma OAI.TensorCriterion.E_isometry line 99
  16. lemma OAI.TensorCriterion.composite_apply line 104
  17. lemma OAI.TensorCriterion.choi_trace_pairing line 116
  18. lemma OAI.TensorCriterion.trace_projector_mul line 135
  19. lemma OAI.TensorCriterion.Z_psd line 140
  20. lemma OAI.TensorCriterion.Z_trace_pairing line 143
  21. lemma OAI.TensorCriterion.Z_quadratic line 150
  22. lemma OAI.TensorCriterion.det_zero_of_rank_lt line 156
  23. lemma OAI.TensorCriterion.rank_loss_kernel line 162
  24. lemma OAI.TensorCriterion.Z_ne_zero line 168