OAI/Analysis/Quantum/PPTSquare/QuadraticCriterion.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TensorCriterion.symExponent line 13
  2. lemma OAI.TensorCriterion.symExponent_injective line 16
  3. lemma OAI.TensorCriterion.symExponent_degree line 26
  4. def OAI.TensorCriterion.quadratic line 29
  5. lemma OAI.TensorCriterion.quadratic_homogeneous line 32
  6. lemma OAI.TensorCriterion.quadratic_coeff line 37
  7. lemma OAI.TensorCriterion.quadratic_ne line 41
  8. lemma OAI.TensorCriterion.quadratic_eval line 50
  9. lemma OAI.TensorCriterion.product_dot_product line 61
  10. lemma OAI.TensorCriterion.product_ne_factors line 73
  11. lemma OAI.TensorCriterion.range_product_quadratic line 79
  12. lemma OAI.TensorCriterion.no_product_in_range line 88
  13. lemma OAI.TensorCriterion.range_mul_self_conjTranspose line 119
  14. def OAI.TensorCriterion.concatenate line 127
  15. lemma OAI.TensorCriterion.concatenate_mul line 131
  16. lemma OAI.TensorCriterion.sqrt_mul_conjTranspose line 137
  17. lemma OAI.TensorCriterion.separable_nonzero_product line 142
  18. theorem OAI.TensorCriterion.tensor_criterion line 179