OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical165.lean

GitHub source file

126 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw5280 line 22
  2. def OAI.MUB6.Certificate.PairSemantics.raw5280step0 line 24
  3. def OAI.MUB6.Certificate.PairSemantics.raw5280step1 line 26
  4. def OAI.MUB6.Certificate.PairSemantics.raw5280step2 line 28
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical5280 line 30
  6. def OAI.MUB6.Certificate.PairSemantics.raw5281 line 48
  7. def OAI.MUB6.Certificate.PairSemantics.raw5281step0 line 50
  8. def OAI.MUB6.Certificate.PairSemantics.raw5281step1 line 52
  9. def OAI.MUB6.Certificate.PairSemantics.raw5281step2 line 54
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical5281 line 56
  11. def OAI.MUB6.Certificate.PairSemantics.raw5282 line 74
  12. def OAI.MUB6.Certificate.PairSemantics.raw5282step0 line 76
  13. def OAI.MUB6.Certificate.PairSemantics.raw5282step1 line 78
  14. def OAI.MUB6.Certificate.PairSemantics.raw5282step2 line 80
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical5282 line 82
  16. def OAI.MUB6.Certificate.PairSemantics.raw5283 line 100
  17. def OAI.MUB6.Certificate.PairSemantics.raw5283step0 line 102
  18. def OAI.MUB6.Certificate.PairSemantics.raw5283step1 line 104
  19. def OAI.MUB6.Certificate.PairSemantics.raw5283step2 line 106
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical5283 line 108
  21. def OAI.MUB6.Certificate.PairSemantics.raw5284 line 126
  22. def OAI.MUB6.Certificate.PairSemantics.raw5284step0 line 128
  23. def OAI.MUB6.Certificate.PairSemantics.raw5284step1 line 130
  24. def OAI.MUB6.Certificate.PairSemantics.raw5284step2 line 132
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical5284 line 134
  26. def OAI.MUB6.Certificate.PairSemantics.raw5285 line 152
  27. def OAI.MUB6.Certificate.PairSemantics.raw5285step0 line 154
  28. def OAI.MUB6.Certificate.PairSemantics.raw5285step1 line 156
  29. def OAI.MUB6.Certificate.PairSemantics.raw5285step2 line 158
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical5285 line 160
  31. def OAI.MUB6.Certificate.PairSemantics.raw5286 line 178
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical5286 line 180
  33. def OAI.MUB6.Certificate.PairSemantics.raw5287 line 184
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical5287 line 186
  35. def OAI.MUB6.Certificate.PairSemantics.raw5288 line 190
  36. def OAI.MUB6.Certificate.PairSemantics.raw5288step0 line 192
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical5288 line 194
  38. def OAI.MUB6.Certificate.PairSemantics.raw5289 line 203
  39. def OAI.MUB6.Certificate.PairSemantics.raw5289step0 line 205
  40. def OAI.MUB6.Certificate.PairSemantics.raw5289step1 line 207
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical5289 line 209
  42. def OAI.MUB6.Certificate.PairSemantics.raw5290 line 222
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical5290 line 224
  44. def OAI.MUB6.Certificate.PairSemantics.raw5291 line 228
  45. def OAI.MUB6.Certificate.PairSemantics.raw5291step0 line 230
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical5291 line 232
  47. def OAI.MUB6.Certificate.PairSemantics.raw5292 line 241
  48. def OAI.MUB6.Certificate.PairSemantics.raw5292step0 line 243
  49. def OAI.MUB6.Certificate.PairSemantics.raw5292step1 line 245
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical5292 line 247
  51. def OAI.MUB6.Certificate.PairSemantics.raw5293 line 260
  52. def OAI.MUB6.Certificate.PairSemantics.raw5293step0 line 262
  53. def OAI.MUB6.Certificate.PairSemantics.raw5293step1 line 264
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical5293 line 266
  55. def OAI.MUB6.Certificate.PairSemantics.raw5294 line 279
  56. def OAI.MUB6.Certificate.PairSemantics.raw5294step0 line 281
  57. def OAI.MUB6.Certificate.PairSemantics.raw5294step1 line 283
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical5294 line 285
  59. def OAI.MUB6.Certificate.PairSemantics.raw5295 line 298
  60. def OAI.MUB6.Certificate.PairSemantics.raw5295step0 line 300
  61. def OAI.MUB6.Certificate.PairSemantics.raw5295step1 line 302
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical5295 line 304
  63. def OAI.MUB6.Certificate.PairSemantics.raw5296 line 317
  64. def OAI.MUB6.Certificate.PairSemantics.raw5296step0 line 319
  65. def OAI.MUB6.Certificate.PairSemantics.raw5296step1 line 321
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical5296 line 323
  67. def OAI.MUB6.Certificate.PairSemantics.raw5297 line 336
  68. def OAI.MUB6.Certificate.PairSemantics.raw5297step0 line 338
  69. def OAI.MUB6.Certificate.PairSemantics.raw5297step1 line 340
  70. def OAI.MUB6.Certificate.PairSemantics.raw5297step2 line 342
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical5297 line 344
  72. def OAI.MUB6.Certificate.PairSemantics.raw5298 line 361
  73. def OAI.MUB6.Certificate.PairSemantics.raw5298step0 line 363
  74. def OAI.MUB6.Certificate.PairSemantics.raw5298step1 line 365
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical5298 line 367
  76. def OAI.MUB6.Certificate.PairSemantics.raw5299 line 380
  77. def OAI.MUB6.Certificate.PairSemantics.raw5299step0 line 382
  78. def OAI.MUB6.Certificate.PairSemantics.raw5299step1 line 384
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical5299 line 386
  80. def OAI.MUB6.Certificate.PairSemantics.raw5300 line 399
  81. def OAI.MUB6.Certificate.PairSemantics.raw5300step0 line 401
  82. def OAI.MUB6.Certificate.PairSemantics.raw5300step1 line 403
  83. def OAI.MUB6.Certificate.PairSemantics.raw5300step2 line 405
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical5300 line 407
  85. def OAI.MUB6.Certificate.PairSemantics.raw5301 line 424
  86. def OAI.MUB6.Certificate.PairSemantics.raw5301step0 line 426
  87. def OAI.MUB6.Certificate.PairSemantics.raw5301step1 line 428
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical5301 line 430
  89. def OAI.MUB6.Certificate.PairSemantics.raw5302 line 443
  90. def OAI.MUB6.Certificate.PairSemantics.raw5302step0 line 445
  91. def OAI.MUB6.Certificate.PairSemantics.raw5302step1 line 447
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical5302 line 449
  93. def OAI.MUB6.Certificate.PairSemantics.raw5303 line 462
  94. def OAI.MUB6.Certificate.PairSemantics.raw5303step0 line 464
  95. def OAI.MUB6.Certificate.PairSemantics.raw5303step1 line 466
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical5303 line 468
  97. def OAI.MUB6.Certificate.PairSemantics.raw5304 line 481
  98. def OAI.MUB6.Certificate.PairSemantics.raw5304step0 line 483
  99. def OAI.MUB6.Certificate.PairSemantics.raw5304step1 line 485
  100. def OAI.MUB6.Certificate.PairSemantics.raw5304step2 line 487
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical5304 line 489
  102. def OAI.MUB6.Certificate.PairSemantics.raw5305 line 506
  103. def OAI.MUB6.Certificate.PairSemantics.raw5305step0 line 508
  104. def OAI.MUB6.Certificate.PairSemantics.raw5305step1 line 510
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical5305 line 512
  106. def OAI.MUB6.Certificate.PairSemantics.raw5306 line 525
  107. def OAI.MUB6.Certificate.PairSemantics.raw5306step0 line 527
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical5306 line 529
  109. def OAI.MUB6.Certificate.PairSemantics.raw5307 line 538
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical5307 line 540
  111. def OAI.MUB6.Certificate.PairSemantics.raw5308 line 544
  112. def OAI.MUB6.Certificate.PairSemantics.raw5308step0 line 546
  113. def OAI.MUB6.Certificate.PairSemantics.raw5308step1 line 548
  114. def OAI.MUB6.Certificate.PairSemantics.raw5308step2 line 550
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical5308 line 552
  116. def OAI.MUB6.Certificate.PairSemantics.raw5309 line 569
  117. def OAI.MUB6.Certificate.PairSemantics.raw5309step0 line 571
  118. def OAI.MUB6.Certificate.PairSemantics.raw5309step1 line 573
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical5309 line 575
  120. def OAI.MUB6.Certificate.PairSemantics.raw5310 line 588
  121. def OAI.MUB6.Certificate.PairSemantics.raw5310step0 line 590
  122. theorem OAI.MUB6.Certificate.PairSemantics.canonical5310 line 592
  123. def OAI.MUB6.Certificate.PairSemantics.raw5311 line 601
  124. def OAI.MUB6.Certificate.PairSemantics.raw5311step0 line 603
  125. def OAI.MUB6.Certificate.PairSemantics.raw5311step1 line 605
  126. theorem OAI.MUB6.Certificate.PairSemantics.canonical5311 line 607