OAI/Analysis/CharacterCriterion/Pauli.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KirchbergRordam.Pauli.M2 line 11
  2. def OAI.KirchbergRordam.Pauli.e line 13
  3. lemma OAI.KirchbergRordam.Pauli.e_zero line 15
  4. lemma OAI.KirchbergRordam.Pauli.e_star line 16
  5. lemma OAI.KirchbergRordam.Pauli.e_square line 18
  6. lemma OAI.KirchbergRordam.Pauli.e_gram line 21
  7. lemma OAI.KirchbergRordam.Pauli.trace_mul line 23
  8. def OAI.KirchbergRordam.Pauli.coeff line 27
  9. lemma OAI.KirchbergRordam.Pauli.coeff_apply line 29
  10. lemma OAI.KirchbergRordam.Pauli.coeff_e line 30
  11. lemma OAI.KirchbergRordam.Pauli.independent line 34
  12. def OAI.KirchbergRordam.Pauli.basis line 40
  13. lemma OAI.KirchbergRordam.Pauli.basis_apply line 44
  14. lemma OAI.KirchbergRordam.Pauli.coeff_sum line 46
  15. def OAI.KirchbergRordam.PauliPower.Row line 56
  16. def OAI.KirchbergRordam.PauliPower.Label line 60
  17. instance OAI.KirchbergRordam.PauliPower.rowFintype line 64
  18. instance OAI.KirchbergRordam.PauliPower.rowDecidableEq line 67
  19. instance OAI.KirchbergRordam.PauliPower.labelFintype line 70
  20. instance OAI.KirchbergRordam.PauliPower.labelDecidableEq line 73
  21. abbrev OAI.KirchbergRordam.PauliPower.Mat line 77
  22. def OAI.KirchbergRordam.PauliPower.e line 79
  23. lemma OAI.KirchbergRordam.PauliPower.row_card line 83
  24. lemma OAI.KirchbergRordam.PauliPower.label_card line 90
  25. lemma OAI.KirchbergRordam.PauliPower.e_star line 98
  26. lemma OAI.KirchbergRordam.PauliPower.e_square line 109
  27. lemma OAI.KirchbergRordam.PauliPower.trace_mul line 118
  28. def OAI.KirchbergRordam.PauliPower.coeff line 134
  29. lemma OAI.KirchbergRordam.PauliPower.coeff_apply line 136
  30. lemma OAI.KirchbergRordam.PauliPower.coeff_e line 138
  31. lemma OAI.KirchbergRordam.PauliPower.independent line 142
  32. def OAI.KirchbergRordam.PauliPower.basis line 148
  33. lemma OAI.KirchbergRordam.PauliPower.basis_apply line 154
  34. lemma OAI.KirchbergRordam.PauliPower.coeff_sum line 155
  35. abbrev OAI.KirchbergRordam.PauliPower.CMat line 161
  36. instance OAI.KirchbergRordam.PauliPower.(instance at line 162) line 162
  37. def OAI.KirchbergRordam.PauliPower.ce line 164
  38. def OAI.KirchbergRordam.PauliPower.ccoeff line 165
  39. lemma OAI.KirchbergRordam.PauliPower.ccoeff_ce line 167
  40. lemma OAI.KirchbergRordam.PauliPower.ccoeff_sum line 169
  41. lemma OAI.KirchbergRordam.PauliPower.ce_star line 171
  42. lemma OAI.KirchbergRordam.PauliPower.ce_square line 173
  43. lemma OAI.KirchbergRordam.MatrixTensor.algebra_legs_commute line 182
  44. lemma OAI.KirchbergRordam.MatrixTensor.legs_commute line 189
  45. lemma OAI.KirchbergRordam.MatrixTensor.algebra_legs_product line 194
  46. lemma OAI.KirchbergRordam.MatrixTensor.legs_product line 201
  47. def OAI.KirchbergRordam.PauliSupport.partner line 211
  48. lemma OAI.KirchbergRordam.PauliSupport.anti line 212
  49. def OAI.KirchbergRordam.PauliSupport.coord line 220
  50. def OAI.KirchbergRordam.PauliSupport.leg line 224
  51. lemma OAI.KirchbergRordam.PauliSupport.anti_leg line 229
  52. lemma OAI.KirchbergRordam.PauliSupport.trace_zero_of_anti line 255
  53. lemma OAI.KirchbergRordam.PauliSupport.coeff_zero line 269
  54. def OAI.KirchbergRordam.PauliPower.zeroLabel line 277
  55. lemma OAI.KirchbergRordam.PauliPower.e_zeroLabel line 281
  56. lemma OAI.KirchbergRordam.PauliPower.coord_zero_iff line 289
  57. lemma OAI.KirchbergRordam.PauliPower.exists_anti line 309
  58. class OAI.KirchbergRordam.GenericRW.Size line 321
  59. instance OAI.KirchbergRordam.GenericRW.(instance at line 324) line 324
  60. class OAI.KirchbergRordam.GenericRW.PauliData line 332
  61. instance OAI.KirchbergRordam.GenericRW.(instance at line 348) line 348
  62. abbrev OAI.KirchbergRordam.GenericRW.powerSize line 351
  63. def OAI.KirchbergRordam.GenericRW.rowEquiv line 354
  64. def OAI.KirchbergRordam.GenericRW.rowReindex line 358
  65. lemma OAI.KirchbergRordam.GenericRW.reindex_trace line 366
  66. def OAI.KirchbergRordam.GenericRW.powerPauliData line 374