OAI/InformationTheory/QuantumCircuit/PauliBasis.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

The tensor-product Pauli basis.

  1. def OAI.QAC.pauli line 13
  2. lemma OAI.QAC.pauli_zero line 17
  3. lemma OAI.QAC.pauli_unitary line 19
  4. lemma OAI.QAC.pauli_trace_star line 24
  5. lemma OAI.QAC.pauli_complete line 27
  6. def OAI.QAC.pauliTensor line 33
  7. def OAI.QAC.pauliSupport line 36
  8. lemma OAI.QAC.pauliTensor_unitary line 39
  9. lemma OAI.QAC.pauliTensor_complete line 42
  10. def OAI.QAC.pauliCoefficient line 60
  11. lemma OAI.QAC.sum_three_rotate line 63
  12. lemma OAI.QAC.matrix_delta_sum line 71
  13. lemma OAI.QAC.pauli_expansion line 77
  14. lemma OAI.QAC.pauliCoefficient_add line 109
  15. lemma OAI.QAC.pauliCoefficient_smul line 113
  16. lemma OAI.QAC.tensorMatrix_trace line 117
  17. lemma OAI.QAC.pauliCoefficient_supported_zero line 122
  18. lemma OAI.QAC.pauliCoefficient_degree_zero line 135
  19. lemma OAI.QAC.pauliCoefficient_norm line 150