OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical112.lean

GitHub source file

132 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3584 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw3584step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw3584step1 line 23
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3584 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw3585 line 38
  6. def OAI.MUB6.Certificate.PairSemantics.raw3585step0 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw3585step1 line 42
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical3585 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw3586 line 57
  10. def OAI.MUB6.Certificate.PairSemantics.raw3586step0 line 59
  11. def OAI.MUB6.Certificate.PairSemantics.raw3586step1 line 61
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical3586 line 63
  13. def OAI.MUB6.Certificate.PairSemantics.raw3587 line 76
  14. def OAI.MUB6.Certificate.PairSemantics.raw3587step0 line 78
  15. def OAI.MUB6.Certificate.PairSemantics.raw3587step1 line 80
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical3587 line 82
  17. def OAI.MUB6.Certificate.PairSemantics.raw3588 line 95
  18. def OAI.MUB6.Certificate.PairSemantics.raw3588step0 line 97
  19. def OAI.MUB6.Certificate.PairSemantics.raw3588step1 line 99
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical3588 line 101
  21. def OAI.MUB6.Certificate.PairSemantics.raw3589 line 114
  22. def OAI.MUB6.Certificate.PairSemantics.raw3589step0 line 116
  23. def OAI.MUB6.Certificate.PairSemantics.raw3589step1 line 118
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical3589 line 120
  25. def OAI.MUB6.Certificate.PairSemantics.raw3590 line 133
  26. def OAI.MUB6.Certificate.PairSemantics.raw3590step0 line 135
  27. def OAI.MUB6.Certificate.PairSemantics.raw3590step1 line 137
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical3590 line 139
  29. def OAI.MUB6.Certificate.PairSemantics.raw3591 line 152
  30. def OAI.MUB6.Certificate.PairSemantics.raw3591step0 line 154
  31. def OAI.MUB6.Certificate.PairSemantics.raw3591step1 line 156
  32. def OAI.MUB6.Certificate.PairSemantics.raw3591step2 line 158
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical3591 line 160
  34. def OAI.MUB6.Certificate.PairSemantics.raw3592 line 177
  35. def OAI.MUB6.Certificate.PairSemantics.raw3592step0 line 179
  36. def OAI.MUB6.Certificate.PairSemantics.raw3592step1 line 181
  37. def OAI.MUB6.Certificate.PairSemantics.raw3592step2 line 183
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical3592 line 185
  39. def OAI.MUB6.Certificate.PairSemantics.raw3593 line 202
  40. def OAI.MUB6.Certificate.PairSemantics.raw3593step0 line 204
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical3593 line 206
  42. def OAI.MUB6.Certificate.PairSemantics.raw3594 line 215
  43. def OAI.MUB6.Certificate.PairSemantics.raw3594step0 line 217
  44. def OAI.MUB6.Certificate.PairSemantics.raw3594step1 line 219
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical3594 line 221
  46. def OAI.MUB6.Certificate.PairSemantics.raw3595 line 234
  47. def OAI.MUB6.Certificate.PairSemantics.raw3595step0 line 236
  48. def OAI.MUB6.Certificate.PairSemantics.raw3595step1 line 238
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical3595 line 240
  50. def OAI.MUB6.Certificate.PairSemantics.raw3596 line 253
  51. def OAI.MUB6.Certificate.PairSemantics.raw3596step0 line 255
  52. def OAI.MUB6.Certificate.PairSemantics.raw3596step1 line 257
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical3596 line 259
  54. def OAI.MUB6.Certificate.PairSemantics.raw3597 line 272
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical3597 line 274
  56. def OAI.MUB6.Certificate.PairSemantics.raw3598 line 278
  57. def OAI.MUB6.Certificate.PairSemantics.raw3598step0 line 280
  58. def OAI.MUB6.Certificate.PairSemantics.raw3598step1 line 282
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical3598 line 284
  60. def OAI.MUB6.Certificate.PairSemantics.raw3599 line 297
  61. def OAI.MUB6.Certificate.PairSemantics.raw3599step0 line 299
  62. def OAI.MUB6.Certificate.PairSemantics.raw3599step1 line 301
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical3599 line 303
  64. def OAI.MUB6.Certificate.PairSemantics.raw3600 line 316
  65. def OAI.MUB6.Certificate.PairSemantics.raw3600step0 line 318
  66. def OAI.MUB6.Certificate.PairSemantics.raw3600step1 line 320
  67. def OAI.MUB6.Certificate.PairSemantics.raw3600step2 line 322
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical3600 line 324
  69. def OAI.MUB6.Certificate.PairSemantics.raw3601 line 341
  70. def OAI.MUB6.Certificate.PairSemantics.raw3601step0 line 343
  71. def OAI.MUB6.Certificate.PairSemantics.raw3601step1 line 345
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical3601 line 347
  73. def OAI.MUB6.Certificate.PairSemantics.raw3602 line 360
  74. def OAI.MUB6.Certificate.PairSemantics.raw3602step0 line 362
  75. def OAI.MUB6.Certificate.PairSemantics.raw3602step1 line 364
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical3602 line 366
  77. def OAI.MUB6.Certificate.PairSemantics.raw3603 line 379
  78. def OAI.MUB6.Certificate.PairSemantics.raw3603step0 line 381
  79. def OAI.MUB6.Certificate.PairSemantics.raw3603step1 line 383
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical3603 line 385
  81. def OAI.MUB6.Certificate.PairSemantics.raw3604 line 398
  82. def OAI.MUB6.Certificate.PairSemantics.raw3604step0 line 400
  83. def OAI.MUB6.Certificate.PairSemantics.raw3604step1 line 402
  84. def OAI.MUB6.Certificate.PairSemantics.raw3604step2 line 404
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical3604 line 406
  86. def OAI.MUB6.Certificate.PairSemantics.raw3605 line 423
  87. def OAI.MUB6.Certificate.PairSemantics.raw3605step0 line 425
  88. def OAI.MUB6.Certificate.PairSemantics.raw3605step1 line 427
  89. def OAI.MUB6.Certificate.PairSemantics.raw3605step2 line 429
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical3605 line 431
  91. def OAI.MUB6.Certificate.PairSemantics.raw3606 line 448
  92. def OAI.MUB6.Certificate.PairSemantics.raw3606step0 line 450
  93. def OAI.MUB6.Certificate.PairSemantics.raw3606step1 line 452
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical3606 line 454
  95. def OAI.MUB6.Certificate.PairSemantics.raw3607 line 467
  96. def OAI.MUB6.Certificate.PairSemantics.raw3607step0 line 469
  97. def OAI.MUB6.Certificate.PairSemantics.raw3607step1 line 471
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical3607 line 473
  99. def OAI.MUB6.Certificate.PairSemantics.raw3608 line 486
  100. def OAI.MUB6.Certificate.PairSemantics.raw3608step0 line 488
  101. def OAI.MUB6.Certificate.PairSemantics.raw3608step1 line 490
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical3608 line 492
  103. def OAI.MUB6.Certificate.PairSemantics.raw3609 line 505
  104. def OAI.MUB6.Certificate.PairSemantics.raw3609step0 line 507
  105. def OAI.MUB6.Certificate.PairSemantics.raw3609step1 line 509
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical3609 line 511
  107. def OAI.MUB6.Certificate.PairSemantics.raw3610 line 524
  108. def OAI.MUB6.Certificate.PairSemantics.raw3610step0 line 526
  109. def OAI.MUB6.Certificate.PairSemantics.raw3610step1 line 528
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical3610 line 530
  111. def OAI.MUB6.Certificate.PairSemantics.raw3611 line 543
  112. def OAI.MUB6.Certificate.PairSemantics.raw3611step0 line 545
  113. def OAI.MUB6.Certificate.PairSemantics.raw3611step1 line 547
  114. def OAI.MUB6.Certificate.PairSemantics.raw3611step2 line 549
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical3611 line 551
  116. def OAI.MUB6.Certificate.PairSemantics.raw3612 line 568
  117. def OAI.MUB6.Certificate.PairSemantics.raw3612step0 line 570
  118. def OAI.MUB6.Certificate.PairSemantics.raw3612step1 line 572
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical3612 line 574
  120. def OAI.MUB6.Certificate.PairSemantics.raw3613 line 587
  121. def OAI.MUB6.Certificate.PairSemantics.raw3613step0 line 589
  122. def OAI.MUB6.Certificate.PairSemantics.raw3613step1 line 591
  123. theorem OAI.MUB6.Certificate.PairSemantics.canonical3613 line 593
  124. def OAI.MUB6.Certificate.PairSemantics.raw3614 line 606
  125. def OAI.MUB6.Certificate.PairSemantics.raw3614step0 line 608
  126. def OAI.MUB6.Certificate.PairSemantics.raw3614step1 line 610
  127. def OAI.MUB6.Certificate.PairSemantics.raw3614step2 line 612
  128. theorem OAI.MUB6.Certificate.PairSemantics.canonical3614 line 614
  129. def OAI.MUB6.Certificate.PairSemantics.raw3615 line 631
  130. def OAI.MUB6.Certificate.PairSemantics.raw3615step0 line 633
  131. def OAI.MUB6.Certificate.PairSemantics.raw3615step1 line 635
  132. theorem OAI.MUB6.Certificate.PairSemantics.canonical3615 line 637