OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical255.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8160 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw8160step0 line 20
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical8160 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw8161 line 31
  5. def OAI.MUB6.Certificate.PairSemantics.raw8161step0 line 33
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical8161 line 35
  7. def OAI.MUB6.Certificate.PairSemantics.raw8162 line 44
  8. def OAI.MUB6.Certificate.PairSemantics.raw8162step0 line 46
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical8162 line 48
  10. def OAI.MUB6.Certificate.PairSemantics.raw8163 line 57
  11. def OAI.MUB6.Certificate.PairSemantics.raw8163step0 line 59
  12. def OAI.MUB6.Certificate.PairSemantics.raw8163step1 line 61
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical8163 line 63
  14. def OAI.MUB6.Certificate.PairSemantics.raw8164 line 76
  15. def OAI.MUB6.Certificate.PairSemantics.raw8164step0 line 78
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical8164 line 80
  17. def OAI.MUB6.Certificate.PairSemantics.raw8165 line 89
  18. def OAI.MUB6.Certificate.PairSemantics.raw8165step0 line 91
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical8165 line 93
  20. def OAI.MUB6.Certificate.PairSemantics.raw8166 line 102
  21. def OAI.MUB6.Certificate.PairSemantics.raw8166step0 line 104
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical8166 line 106
  23. def OAI.MUB6.Certificate.PairSemantics.raw8167 line 115
  24. def OAI.MUB6.Certificate.PairSemantics.raw8167step0 line 117
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical8167 line 119
  26. def OAI.MUB6.Certificate.PairSemantics.raw8168 line 128
  27. def OAI.MUB6.Certificate.PairSemantics.raw8168step0 line 130
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical8168 line 132
  29. def OAI.MUB6.Certificate.PairSemantics.raw8169 line 141
  30. def OAI.MUB6.Certificate.PairSemantics.raw8169step0 line 143
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical8169 line 145
  32. def OAI.MUB6.Certificate.PairSemantics.raw8170 line 154
  33. def OAI.MUB6.Certificate.PairSemantics.raw8170step0 line 156
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical8170 line 158
  35. def OAI.MUB6.Certificate.PairSemantics.raw8171 line 167
  36. def OAI.MUB6.Certificate.PairSemantics.raw8171step0 line 169
  37. def OAI.MUB6.Certificate.PairSemantics.raw8171step1 line 171
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical8171 line 173
  39. def OAI.MUB6.Certificate.PairSemantics.raw8172 line 187
  40. def OAI.MUB6.Certificate.PairSemantics.raw8172step0 line 189
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical8172 line 191
  42. def OAI.MUB6.Certificate.PairSemantics.raw8173 line 200
  43. def OAI.MUB6.Certificate.PairSemantics.raw8173step0 line 202
  44. def OAI.MUB6.Certificate.PairSemantics.raw8173step1 line 204
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical8173 line 206
  46. def OAI.MUB6.Certificate.PairSemantics.raw8174 line 219
  47. def OAI.MUB6.Certificate.PairSemantics.raw8174step0 line 221
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical8174 line 223
  49. def OAI.MUB6.Certificate.PairSemantics.raw8175 line 232
  50. def OAI.MUB6.Certificate.PairSemantics.raw8175step0 line 234
  51. def OAI.MUB6.Certificate.PairSemantics.raw8175step1 line 236
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical8175 line 238
  53. def OAI.MUB6.Certificate.PairSemantics.raw8176 line 251
  54. def OAI.MUB6.Certificate.PairSemantics.raw8176step0 line 253
  55. def OAI.MUB6.Certificate.PairSemantics.raw8176step1 line 255
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical8176 line 257
  57. def OAI.MUB6.Certificate.PairSemantics.raw8177 line 270
  58. def OAI.MUB6.Certificate.PairSemantics.raw8177step0 line 272
  59. def OAI.MUB6.Certificate.PairSemantics.raw8177step1 line 274
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical8177 line 276
  61. def OAI.MUB6.Certificate.PairSemantics.raw8178 line 289
  62. def OAI.MUB6.Certificate.PairSemantics.raw8178step0 line 291
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical8178 line 293
  64. def OAI.MUB6.Certificate.PairSemantics.raw8179 line 302
  65. def OAI.MUB6.Certificate.PairSemantics.raw8179step0 line 304
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical8179 line 306
  67. def OAI.MUB6.Certificate.PairSemantics.raw8180 line 315
  68. def OAI.MUB6.Certificate.PairSemantics.raw8180step0 line 317
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical8180 line 319
  70. def OAI.MUB6.Certificate.PairSemantics.raw8181 line 328
  71. def OAI.MUB6.Certificate.PairSemantics.raw8181step0 line 330
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical8181 line 332
  73. def OAI.MUB6.Certificate.PairSemantics.raw8182 line 341
  74. def OAI.MUB6.Certificate.PairSemantics.raw8182step0 line 343
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical8182 line 345
  76. def OAI.MUB6.Certificate.PairSemantics.raw8183 line 354
  77. def OAI.MUB6.Certificate.PairSemantics.raw8183step0 line 356
  78. def OAI.MUB6.Certificate.PairSemantics.raw8183step1 line 358
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical8183 line 360
  80. def OAI.MUB6.Certificate.PairSemantics.raw8184 line 374
  81. def OAI.MUB6.Certificate.PairSemantics.raw8184step0 line 376
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical8184 line 378
  83. def OAI.MUB6.Certificate.PairSemantics.raw8185 line 387
  84. def OAI.MUB6.Certificate.PairSemantics.raw8185step0 line 389
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical8185 line 391
  86. def OAI.MUB6.Certificate.PairSemantics.raw8186 line 400
  87. def OAI.MUB6.Certificate.PairSemantics.raw8186step0 line 402
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical8186 line 404
  89. def OAI.MUB6.Certificate.PairSemantics.raw8187 line 413
  90. def OAI.MUB6.Certificate.PairSemantics.raw8187step0 line 415
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical8187 line 417
  92. def OAI.MUB6.Certificate.PairSemantics.raw8188 line 426
  93. def OAI.MUB6.Certificate.PairSemantics.raw8188step0 line 428
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical8188 line 430
  95. def OAI.MUB6.Certificate.PairSemantics.raw8189 line 439
  96. def OAI.MUB6.Certificate.PairSemantics.raw8189step0 line 441
  97. def OAI.MUB6.Certificate.PairSemantics.raw8189step1 line 443
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical8189 line 445
  99. def OAI.MUB6.Certificate.PairSemantics.raw8190 line 458
  100. def OAI.MUB6.Certificate.PairSemantics.raw8190step0 line 460
  101. def OAI.MUB6.Certificate.PairSemantics.raw8190step1 line 462
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical8190 line 464
  103. def OAI.MUB6.Certificate.PairSemantics.raw8191 line 477
  104. def OAI.MUB6.Certificate.PairSemantics.raw8191step0 line 479
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical8191 line 481