OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical203.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6496 line 12
  2. def OAI.MUB6.Certificate.PairSemantics.raw6496step0 line 14
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical6496 line 16
  4. def OAI.MUB6.Certificate.PairSemantics.raw6497 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw6497step0 line 27
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical6497 line 29
  7. def OAI.MUB6.Certificate.PairSemantics.raw6498 line 38
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical6498 line 40
  9. def OAI.MUB6.Certificate.PairSemantics.raw6499 line 44
  10. def OAI.MUB6.Certificate.PairSemantics.raw6499step0 line 46
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical6499 line 48
  12. def OAI.MUB6.Certificate.PairSemantics.raw6500 line 57
  13. def OAI.MUB6.Certificate.PairSemantics.raw6500step0 line 59
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical6500 line 61
  15. def OAI.MUB6.Certificate.PairSemantics.raw6501 line 71
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical6501 line 73
  17. def OAI.MUB6.Certificate.PairSemantics.raw6502 line 77
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical6502 line 79
  19. def OAI.MUB6.Certificate.PairSemantics.raw6503 line 83
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical6503 line 85
  21. def OAI.MUB6.Certificate.PairSemantics.raw6504 line 89
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical6504 line 91
  23. def OAI.MUB6.Certificate.PairSemantics.raw6505 line 95
  24. def OAI.MUB6.Certificate.PairSemantics.raw6505step0 line 97
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical6505 line 99
  26. def OAI.MUB6.Certificate.PairSemantics.raw6506 line 108
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical6506 line 110
  28. def OAI.MUB6.Certificate.PairSemantics.raw6507 line 114
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical6507 line 116
  30. def OAI.MUB6.Certificate.PairSemantics.raw6508 line 120
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical6508 line 122
  32. def OAI.MUB6.Certificate.PairSemantics.raw6509 line 126
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical6509 line 128
  34. def OAI.MUB6.Certificate.PairSemantics.raw6510 line 132
  35. def OAI.MUB6.Certificate.PairSemantics.raw6510step0 line 134
  36. def OAI.MUB6.Certificate.PairSemantics.raw6510step1 line 136
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical6510 line 138
  38. def OAI.MUB6.Certificate.PairSemantics.raw6511 line 151
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical6511 line 153
  40. def OAI.MUB6.Certificate.PairSemantics.raw6512 line 157
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical6512 line 159
  42. def OAI.MUB6.Certificate.PairSemantics.raw6513 line 163
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical6513 line 165
  44. def OAI.MUB6.Certificate.PairSemantics.raw6514 line 169
  45. def OAI.MUB6.Certificate.PairSemantics.raw6514step0 line 171
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical6514 line 173
  47. def OAI.MUB6.Certificate.PairSemantics.raw6515 line 182
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical6515 line 184
  49. def OAI.MUB6.Certificate.PairSemantics.raw6516 line 188
  50. def OAI.MUB6.Certificate.PairSemantics.raw6516step0 line 190
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical6516 line 192
  52. def OAI.MUB6.Certificate.PairSemantics.raw6517 line 201
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical6517 line 203
  54. def OAI.MUB6.Certificate.PairSemantics.raw6518 line 207
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical6518 line 209
  56. def OAI.MUB6.Certificate.PairSemantics.raw6519 line 213
  57. def OAI.MUB6.Certificate.PairSemantics.raw6519step0 line 215
  58. def OAI.MUB6.Certificate.PairSemantics.raw6519step1 line 217
  59. def OAI.MUB6.Certificate.PairSemantics.raw6519step2 line 219
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical6519 line 221
  61. def OAI.MUB6.Certificate.PairSemantics.raw6520 line 238
  62. def OAI.MUB6.Certificate.PairSemantics.raw6520step0 line 240
  63. def OAI.MUB6.Certificate.PairSemantics.raw6520step1 line 242
  64. def OAI.MUB6.Certificate.PairSemantics.raw6520step2 line 244
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical6520 line 246
  66. def OAI.MUB6.Certificate.PairSemantics.raw6521 line 263
  67. def OAI.MUB6.Certificate.PairSemantics.raw6521step0 line 265
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical6521 line 267
  69. def OAI.MUB6.Certificate.PairSemantics.raw6522 line 276
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical6522 line 278
  71. def OAI.MUB6.Certificate.PairSemantics.raw6523 line 282
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical6523 line 284
  73. def OAI.MUB6.Certificate.PairSemantics.raw6524 line 288
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical6524 line 290
  75. def OAI.MUB6.Certificate.PairSemantics.raw6525 line 294
  76. def OAI.MUB6.Certificate.PairSemantics.raw6525step0 line 296
  77. def OAI.MUB6.Certificate.PairSemantics.raw6525step1 line 298
  78. def OAI.MUB6.Certificate.PairSemantics.raw6525step2 line 300
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical6525 line 302
  80. def OAI.MUB6.Certificate.PairSemantics.raw6526 line 319
  81. def OAI.MUB6.Certificate.PairSemantics.raw6526step0 line 321
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical6526 line 323
  83. def OAI.MUB6.Certificate.PairSemantics.raw6527 line 332
  84. def OAI.MUB6.Certificate.PairSemantics.raw6527step0 line 334
  85. def OAI.MUB6.Certificate.PairSemantics.raw6527step1 line 336
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical6527 line 338