OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical237.lean

GitHub source file

148 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7584 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw7584step0 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw7584step1 line 20
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7584 line 22
  5. def OAI.MUB6.Certificate.PairSemantics.raw7585 line 35
  6. def OAI.MUB6.Certificate.PairSemantics.raw7585step0 line 37
  7. def OAI.MUB6.Certificate.PairSemantics.raw7585step1 line 39
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical7585 line 41
  9. def OAI.MUB6.Certificate.PairSemantics.raw7586 line 54
  10. def OAI.MUB6.Certificate.PairSemantics.raw7586step0 line 56
  11. def OAI.MUB6.Certificate.PairSemantics.raw7586step1 line 58
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical7586 line 60
  13. def OAI.MUB6.Certificate.PairSemantics.raw7587 line 73
  14. def OAI.MUB6.Certificate.PairSemantics.raw7587step0 line 75
  15. def OAI.MUB6.Certificate.PairSemantics.raw7587step1 line 77
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical7587 line 79
  17. def OAI.MUB6.Certificate.PairSemantics.raw7588 line 92
  18. def OAI.MUB6.Certificate.PairSemantics.raw7588step0 line 94
  19. def OAI.MUB6.Certificate.PairSemantics.raw7588step1 line 96
  20. def OAI.MUB6.Certificate.PairSemantics.raw7588step2 line 98
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical7588 line 100
  22. def OAI.MUB6.Certificate.PairSemantics.raw7589 line 117
  23. def OAI.MUB6.Certificate.PairSemantics.raw7589step0 line 119
  24. def OAI.MUB6.Certificate.PairSemantics.raw7589step1 line 121
  25. def OAI.MUB6.Certificate.PairSemantics.raw7589step2 line 123
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical7589 line 125
  27. def OAI.MUB6.Certificate.PairSemantics.raw7590 line 142
  28. def OAI.MUB6.Certificate.PairSemantics.raw7590step0 line 144
  29. def OAI.MUB6.Certificate.PairSemantics.raw7590step1 line 146
  30. def OAI.MUB6.Certificate.PairSemantics.raw7590step2 line 148
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical7590 line 150
  32. def OAI.MUB6.Certificate.PairSemantics.raw7591 line 167
  33. def OAI.MUB6.Certificate.PairSemantics.raw7591step0 line 169
  34. def OAI.MUB6.Certificate.PairSemantics.raw7591step1 line 171
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical7591 line 173
  36. def OAI.MUB6.Certificate.PairSemantics.raw7592 line 186
  37. def OAI.MUB6.Certificate.PairSemantics.raw7592step0 line 188
  38. def OAI.MUB6.Certificate.PairSemantics.raw7592step1 line 190
  39. def OAI.MUB6.Certificate.PairSemantics.raw7592step2 line 192
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical7592 line 194
  41. def OAI.MUB6.Certificate.PairSemantics.raw7593 line 211
  42. def OAI.MUB6.Certificate.PairSemantics.raw7593step0 line 213
  43. def OAI.MUB6.Certificate.PairSemantics.raw7593step1 line 215
  44. def OAI.MUB6.Certificate.PairSemantics.raw7593step2 line 217
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical7593 line 219
  46. def OAI.MUB6.Certificate.PairSemantics.raw7594 line 236
  47. def OAI.MUB6.Certificate.PairSemantics.raw7594step0 line 238
  48. def OAI.MUB6.Certificate.PairSemantics.raw7594step1 line 240
  49. def OAI.MUB6.Certificate.PairSemantics.raw7594step2 line 242
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical7594 line 244
  51. def OAI.MUB6.Certificate.PairSemantics.raw7595 line 261
  52. def OAI.MUB6.Certificate.PairSemantics.raw7595step0 line 263
  53. def OAI.MUB6.Certificate.PairSemantics.raw7595step1 line 265
  54. def OAI.MUB6.Certificate.PairSemantics.raw7595step2 line 267
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical7595 line 269
  56. def OAI.MUB6.Certificate.PairSemantics.raw7596 line 286
  57. def OAI.MUB6.Certificate.PairSemantics.raw7596step0 line 288
  58. def OAI.MUB6.Certificate.PairSemantics.raw7596step1 line 290
  59. def OAI.MUB6.Certificate.PairSemantics.raw7596step2 line 292
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical7596 line 294
  61. def OAI.MUB6.Certificate.PairSemantics.raw7597 line 311
  62. def OAI.MUB6.Certificate.PairSemantics.raw7597step0 line 313
  63. def OAI.MUB6.Certificate.PairSemantics.raw7597step1 line 315
  64. def OAI.MUB6.Certificate.PairSemantics.raw7597step2 line 317
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical7597 line 319
  66. def OAI.MUB6.Certificate.PairSemantics.raw7598 line 336
  67. def OAI.MUB6.Certificate.PairSemantics.raw7598step0 line 338
  68. def OAI.MUB6.Certificate.PairSemantics.raw7598step1 line 340
  69. def OAI.MUB6.Certificate.PairSemantics.raw7598step2 line 342
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical7598 line 344
  71. def OAI.MUB6.Certificate.PairSemantics.raw7599 line 361
  72. def OAI.MUB6.Certificate.PairSemantics.raw7599step0 line 363
  73. def OAI.MUB6.Certificate.PairSemantics.raw7599step1 line 365
  74. def OAI.MUB6.Certificate.PairSemantics.raw7599step2 line 367
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical7599 line 369
  76. def OAI.MUB6.Certificate.PairSemantics.raw7600 line 386
  77. def OAI.MUB6.Certificate.PairSemantics.raw7600step0 line 388
  78. def OAI.MUB6.Certificate.PairSemantics.raw7600step1 line 390
  79. def OAI.MUB6.Certificate.PairSemantics.raw7600step2 line 392
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical7600 line 394
  81. def OAI.MUB6.Certificate.PairSemantics.raw7601 line 411
  82. def OAI.MUB6.Certificate.PairSemantics.raw7601step0 line 413
  83. def OAI.MUB6.Certificate.PairSemantics.raw7601step1 line 415
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical7601 line 417
  85. def OAI.MUB6.Certificate.PairSemantics.raw7602 line 430
  86. def OAI.MUB6.Certificate.PairSemantics.raw7602step0 line 432
  87. def OAI.MUB6.Certificate.PairSemantics.raw7602step1 line 434
  88. def OAI.MUB6.Certificate.PairSemantics.raw7602step2 line 436
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical7602 line 438
  90. def OAI.MUB6.Certificate.PairSemantics.raw7603 line 455
  91. def OAI.MUB6.Certificate.PairSemantics.raw7603step0 line 457
  92. def OAI.MUB6.Certificate.PairSemantics.raw7603step1 line 459
  93. def OAI.MUB6.Certificate.PairSemantics.raw7603step2 line 461
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical7603 line 463
  95. def OAI.MUB6.Certificate.PairSemantics.raw7604 line 480
  96. def OAI.MUB6.Certificate.PairSemantics.raw7604step0 line 482
  97. def OAI.MUB6.Certificate.PairSemantics.raw7604step1 line 484
  98. def OAI.MUB6.Certificate.PairSemantics.raw7604step2 line 486
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical7604 line 488
  100. def OAI.MUB6.Certificate.PairSemantics.raw7605 line 505
  101. def OAI.MUB6.Certificate.PairSemantics.raw7605step0 line 507
  102. def OAI.MUB6.Certificate.PairSemantics.raw7605step1 line 509
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical7605 line 511
  104. def OAI.MUB6.Certificate.PairSemantics.raw7606 line 524
  105. def OAI.MUB6.Certificate.PairSemantics.raw7606step0 line 526
  106. def OAI.MUB6.Certificate.PairSemantics.raw7606step1 line 528
  107. def OAI.MUB6.Certificate.PairSemantics.raw7606step2 line 530
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical7606 line 532
  109. def OAI.MUB6.Certificate.PairSemantics.raw7607 line 549
  110. def OAI.MUB6.Certificate.PairSemantics.raw7607step0 line 551
  111. def OAI.MUB6.Certificate.PairSemantics.raw7607step1 line 553
  112. def OAI.MUB6.Certificate.PairSemantics.raw7607step2 line 555
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical7607 line 557
  114. def OAI.MUB6.Certificate.PairSemantics.raw7608 line 574
  115. def OAI.MUB6.Certificate.PairSemantics.raw7608step0 line 576
  116. def OAI.MUB6.Certificate.PairSemantics.raw7608step1 line 578
  117. def OAI.MUB6.Certificate.PairSemantics.raw7608step2 line 580
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical7608 line 582
  119. def OAI.MUB6.Certificate.PairSemantics.raw7609 line 599
  120. def OAI.MUB6.Certificate.PairSemantics.raw7609step0 line 601
  121. def OAI.MUB6.Certificate.PairSemantics.raw7609step1 line 603
  122. theorem OAI.MUB6.Certificate.PairSemantics.canonical7609 line 605
  123. def OAI.MUB6.Certificate.PairSemantics.raw7610 line 618
  124. def OAI.MUB6.Certificate.PairSemantics.raw7610step0 line 620
  125. def OAI.MUB6.Certificate.PairSemantics.raw7610step1 line 622
  126. theorem OAI.MUB6.Certificate.PairSemantics.canonical7610 line 624
  127. def OAI.MUB6.Certificate.PairSemantics.raw7611 line 637
  128. def OAI.MUB6.Certificate.PairSemantics.raw7611step0 line 639
  129. def OAI.MUB6.Certificate.PairSemantics.raw7611step1 line 641
  130. def OAI.MUB6.Certificate.PairSemantics.raw7611step2 line 643
  131. theorem OAI.MUB6.Certificate.PairSemantics.canonical7611 line 645
  132. def OAI.MUB6.Certificate.PairSemantics.raw7612 line 662
  133. def OAI.MUB6.Certificate.PairSemantics.raw7612step0 line 664
  134. def OAI.MUB6.Certificate.PairSemantics.raw7612step1 line 666
  135. theorem OAI.MUB6.Certificate.PairSemantics.canonical7612 line 668
  136. def OAI.MUB6.Certificate.PairSemantics.raw7613 line 681
  137. def OAI.MUB6.Certificate.PairSemantics.raw7613step0 line 683
  138. def OAI.MUB6.Certificate.PairSemantics.raw7613step1 line 685
  139. def OAI.MUB6.Certificate.PairSemantics.raw7613step2 line 687
  140. theorem OAI.MUB6.Certificate.PairSemantics.canonical7613 line 689
  141. def OAI.MUB6.Certificate.PairSemantics.raw7614 line 706
  142. def OAI.MUB6.Certificate.PairSemantics.raw7614step0 line 708
  143. def OAI.MUB6.Certificate.PairSemantics.raw7614step1 line 710
  144. theorem OAI.MUB6.Certificate.PairSemantics.canonical7614 line 712
  145. def OAI.MUB6.Certificate.PairSemantics.raw7615 line 725
  146. def OAI.MUB6.Certificate.PairSemantics.raw7615step0 line 727
  147. def OAI.MUB6.Certificate.PairSemantics.raw7615step1 line 729
  148. theorem OAI.MUB6.Certificate.PairSemantics.canonical7615 line 731