OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical108.lean

GitHub source file

121 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3456 line 23
  2. def OAI.MUB6.Certificate.PairSemantics.raw3456step0 line 25
  3. def OAI.MUB6.Certificate.PairSemantics.raw3456step1 line 27
  4. def OAI.MUB6.Certificate.PairSemantics.raw3456step2 line 29
  5. def OAI.MUB6.Certificate.PairSemantics.raw3456step3 line 31
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical3456 line 33
  7. def OAI.MUB6.Certificate.PairSemantics.raw3457 line 55
  8. def OAI.MUB6.Certificate.PairSemantics.raw3457step0 line 57
  9. def OAI.MUB6.Certificate.PairSemantics.raw3457step1 line 59
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical3457 line 61
  11. def OAI.MUB6.Certificate.PairSemantics.raw3458 line 74
  12. def OAI.MUB6.Certificate.PairSemantics.raw3458step0 line 76
  13. def OAI.MUB6.Certificate.PairSemantics.raw3458step1 line 78
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical3458 line 80
  15. def OAI.MUB6.Certificate.PairSemantics.raw3459 line 93
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical3459 line 95
  17. def OAI.MUB6.Certificate.PairSemantics.raw3460 line 99
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical3460 line 101
  19. def OAI.MUB6.Certificate.PairSemantics.raw3461 line 105
  20. def OAI.MUB6.Certificate.PairSemantics.raw3461step0 line 107
  21. def OAI.MUB6.Certificate.PairSemantics.raw3461step1 line 109
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical3461 line 111
  23. def OAI.MUB6.Certificate.PairSemantics.raw3462 line 124
  24. def OAI.MUB6.Certificate.PairSemantics.raw3462step0 line 126
  25. def OAI.MUB6.Certificate.PairSemantics.raw3462step1 line 128
  26. def OAI.MUB6.Certificate.PairSemantics.raw3462step2 line 130
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical3462 line 132
  28. def OAI.MUB6.Certificate.PairSemantics.raw3463 line 150
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical3463 line 152
  30. def OAI.MUB6.Certificate.PairSemantics.raw3464 line 156
  31. def OAI.MUB6.Certificate.PairSemantics.raw3464step0 line 158
  32. def OAI.MUB6.Certificate.PairSemantics.raw3464step1 line 160
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical3464 line 162
  34. def OAI.MUB6.Certificate.PairSemantics.raw3465 line 175
  35. def OAI.MUB6.Certificate.PairSemantics.raw3465step0 line 177
  36. def OAI.MUB6.Certificate.PairSemantics.raw3465step1 line 179
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical3465 line 181
  38. def OAI.MUB6.Certificate.PairSemantics.raw3466 line 194
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical3466 line 196
  40. def OAI.MUB6.Certificate.PairSemantics.raw3467 line 200
  41. def OAI.MUB6.Certificate.PairSemantics.raw3467step0 line 202
  42. def OAI.MUB6.Certificate.PairSemantics.raw3467step1 line 204
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical3467 line 206
  44. def OAI.MUB6.Certificate.PairSemantics.raw3468 line 219
  45. def OAI.MUB6.Certificate.PairSemantics.raw3468step0 line 221
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical3468 line 223
  47. def OAI.MUB6.Certificate.PairSemantics.raw3469 line 232
  48. def OAI.MUB6.Certificate.PairSemantics.raw3469step0 line 234
  49. def OAI.MUB6.Certificate.PairSemantics.raw3469step1 line 236
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical3469 line 238
  51. def OAI.MUB6.Certificate.PairSemantics.raw3470 line 251
  52. def OAI.MUB6.Certificate.PairSemantics.raw3470step0 line 253
  53. def OAI.MUB6.Certificate.PairSemantics.raw3470step1 line 255
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical3470 line 257
  55. def OAI.MUB6.Certificate.PairSemantics.raw3471 line 270
  56. def OAI.MUB6.Certificate.PairSemantics.raw3471step0 line 272
  57. def OAI.MUB6.Certificate.PairSemantics.raw3471step1 line 274
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical3471 line 276
  59. def OAI.MUB6.Certificate.PairSemantics.raw3472 line 289
  60. def OAI.MUB6.Certificate.PairSemantics.raw3472step0 line 291
  61. def OAI.MUB6.Certificate.PairSemantics.raw3472step1 line 293
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical3472 line 295
  63. def OAI.MUB6.Certificate.PairSemantics.raw3473 line 308
  64. def OAI.MUB6.Certificate.PairSemantics.raw3473step0 line 310
  65. def OAI.MUB6.Certificate.PairSemantics.raw3473step1 line 312
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical3473 line 314
  67. def OAI.MUB6.Certificate.PairSemantics.raw3474 line 327
  68. def OAI.MUB6.Certificate.PairSemantics.raw3474step0 line 329
  69. def OAI.MUB6.Certificate.PairSemantics.raw3474step1 line 331
  70. def OAI.MUB6.Certificate.PairSemantics.raw3474step2 line 333
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical3474 line 335
  72. def OAI.MUB6.Certificate.PairSemantics.raw3475 line 352
  73. def OAI.MUB6.Certificate.PairSemantics.raw3475step0 line 354
  74. def OAI.MUB6.Certificate.PairSemantics.raw3475step1 line 356
  75. def OAI.MUB6.Certificate.PairSemantics.raw3475step2 line 358
  76. def OAI.MUB6.Certificate.PairSemantics.raw3475step3 line 360
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical3475 line 362
  78. def OAI.MUB6.Certificate.PairSemantics.raw3476 line 384
  79. def OAI.MUB6.Certificate.PairSemantics.raw3476step0 line 386
  80. def OAI.MUB6.Certificate.PairSemantics.raw3476step1 line 388
  81. def OAI.MUB6.Certificate.PairSemantics.raw3476step2 line 390
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical3476 line 392
  83. def OAI.MUB6.Certificate.PairSemantics.raw3477 line 410
  84. def OAI.MUB6.Certificate.PairSemantics.raw3477step0 line 412
  85. def OAI.MUB6.Certificate.PairSemantics.raw3477step1 line 414
  86. def OAI.MUB6.Certificate.PairSemantics.raw3477step2 line 416
  87. def OAI.MUB6.Certificate.PairSemantics.raw3477step3 line 418
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical3477 line 420
  89. def OAI.MUB6.Certificate.PairSemantics.raw3478 line 442
  90. def OAI.MUB6.Certificate.PairSemantics.raw3478step0 line 444
  91. def OAI.MUB6.Certificate.PairSemantics.raw3478step1 line 446
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical3478 line 448
  93. def OAI.MUB6.Certificate.PairSemantics.raw3479 line 462
  94. def OAI.MUB6.Certificate.PairSemantics.raw3479step0 line 464
  95. def OAI.MUB6.Certificate.PairSemantics.raw3479step1 line 466
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical3479 line 468
  97. def OAI.MUB6.Certificate.PairSemantics.raw3480 line 482
  98. def OAI.MUB6.Certificate.PairSemantics.raw3480step0 line 484
  99. def OAI.MUB6.Certificate.PairSemantics.raw3480step1 line 486
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical3480 line 488
  101. def OAI.MUB6.Certificate.PairSemantics.raw3481 line 501
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical3481 line 503
  103. def OAI.MUB6.Certificate.PairSemantics.raw3482 line 507
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical3482 line 509
  105. def OAI.MUB6.Certificate.PairSemantics.raw3483 line 513
  106. def OAI.MUB6.Certificate.PairSemantics.raw3483step0 line 515
  107. def OAI.MUB6.Certificate.PairSemantics.raw3483step1 line 517
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical3483 line 519
  109. def OAI.MUB6.Certificate.PairSemantics.raw3484 line 532
  110. def OAI.MUB6.Certificate.PairSemantics.raw3484step0 line 534
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical3484 line 536
  112. def OAI.MUB6.Certificate.PairSemantics.raw3485 line 545
  113. def OAI.MUB6.Certificate.PairSemantics.raw3485step0 line 547
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical3485 line 549
  115. def OAI.MUB6.Certificate.PairSemantics.raw3486 line 558
  116. def OAI.MUB6.Certificate.PairSemantics.raw3486step0 line 560
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical3486 line 562
  118. def OAI.MUB6.Certificate.PairSemantics.raw3487 line 571
  119. def OAI.MUB6.Certificate.PairSemantics.raw3487step0 line 573
  120. def OAI.MUB6.Certificate.PairSemantics.raw3487step1 line 575
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical3487 line 577