OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical279.lean

GitHub source file

142 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8928 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw8928step0 line 17
  3. def OAI.MUB6.Certificate.PairSemantics.raw8928step1 line 19
  4. def OAI.MUB6.Certificate.PairSemantics.raw8928step2 line 21
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical8928 line 23
  6. def OAI.MUB6.Certificate.PairSemantics.raw8929 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw8929step0 line 42
  8. def OAI.MUB6.Certificate.PairSemantics.raw8929step1 line 44
  9. def OAI.MUB6.Certificate.PairSemantics.raw8929step2 line 46
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical8929 line 48
  11. def OAI.MUB6.Certificate.PairSemantics.raw8930 line 65
  12. def OAI.MUB6.Certificate.PairSemantics.raw8930step0 line 67
  13. def OAI.MUB6.Certificate.PairSemantics.raw8930step1 line 69
  14. def OAI.MUB6.Certificate.PairSemantics.raw8930step2 line 71
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical8930 line 73
  16. def OAI.MUB6.Certificate.PairSemantics.raw8931 line 90
  17. def OAI.MUB6.Certificate.PairSemantics.raw8931step0 line 92
  18. def OAI.MUB6.Certificate.PairSemantics.raw8931step1 line 94
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical8931 line 96
  20. def OAI.MUB6.Certificate.PairSemantics.raw8932 line 109
  21. def OAI.MUB6.Certificate.PairSemantics.raw8932step0 line 111
  22. def OAI.MUB6.Certificate.PairSemantics.raw8932step1 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw8932step2 line 115
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical8932 line 117
  25. def OAI.MUB6.Certificate.PairSemantics.raw8933 line 134
  26. def OAI.MUB6.Certificate.PairSemantics.raw8933step0 line 136
  27. def OAI.MUB6.Certificate.PairSemantics.raw8933step1 line 138
  28. def OAI.MUB6.Certificate.PairSemantics.raw8933step2 line 140
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical8933 line 142
  30. def OAI.MUB6.Certificate.PairSemantics.raw8934 line 159
  31. def OAI.MUB6.Certificate.PairSemantics.raw8934step0 line 161
  32. def OAI.MUB6.Certificate.PairSemantics.raw8934step1 line 163
  33. def OAI.MUB6.Certificate.PairSemantics.raw8934step2 line 165
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical8934 line 167
  35. def OAI.MUB6.Certificate.PairSemantics.raw8935 line 184
  36. def OAI.MUB6.Certificate.PairSemantics.raw8935step0 line 186
  37. def OAI.MUB6.Certificate.PairSemantics.raw8935step1 line 188
  38. def OAI.MUB6.Certificate.PairSemantics.raw8935step2 line 190
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical8935 line 192
  40. def OAI.MUB6.Certificate.PairSemantics.raw8936 line 209
  41. def OAI.MUB6.Certificate.PairSemantics.raw8936step0 line 211
  42. def OAI.MUB6.Certificate.PairSemantics.raw8936step1 line 213
  43. def OAI.MUB6.Certificate.PairSemantics.raw8936step2 line 215
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical8936 line 217
  45. def OAI.MUB6.Certificate.PairSemantics.raw8937 line 234
  46. def OAI.MUB6.Certificate.PairSemantics.raw8937step0 line 236
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical8937 line 238
  48. def OAI.MUB6.Certificate.PairSemantics.raw8938 line 247
  49. def OAI.MUB6.Certificate.PairSemantics.raw8938step0 line 249
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical8938 line 251
  51. def OAI.MUB6.Certificate.PairSemantics.raw8939 line 260
  52. def OAI.MUB6.Certificate.PairSemantics.raw8939step0 line 262
  53. def OAI.MUB6.Certificate.PairSemantics.raw8939step1 line 264
  54. def OAI.MUB6.Certificate.PairSemantics.raw8939step2 line 266
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical8939 line 268
  56. def OAI.MUB6.Certificate.PairSemantics.raw8940 line 285
  57. def OAI.MUB6.Certificate.PairSemantics.raw8940step0 line 287
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical8940 line 289
  59. def OAI.MUB6.Certificate.PairSemantics.raw8941 line 298
  60. def OAI.MUB6.Certificate.PairSemantics.raw8941step0 line 300
  61. def OAI.MUB6.Certificate.PairSemantics.raw8941step1 line 302
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical8941 line 304
  63. def OAI.MUB6.Certificate.PairSemantics.raw8942 line 317
  64. def OAI.MUB6.Certificate.PairSemantics.raw8942step0 line 319
  65. def OAI.MUB6.Certificate.PairSemantics.raw8942step1 line 321
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical8942 line 323
  67. def OAI.MUB6.Certificate.PairSemantics.raw8943 line 336
  68. def OAI.MUB6.Certificate.PairSemantics.raw8943step0 line 338
  69. def OAI.MUB6.Certificate.PairSemantics.raw8943step1 line 340
  70. def OAI.MUB6.Certificate.PairSemantics.raw8943step2 line 342
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical8943 line 344
  72. def OAI.MUB6.Certificate.PairSemantics.raw8944 line 362
  73. def OAI.MUB6.Certificate.PairSemantics.raw8944step0 line 364
  74. def OAI.MUB6.Certificate.PairSemantics.raw8944step1 line 366
  75. def OAI.MUB6.Certificate.PairSemantics.raw8944step2 line 368
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical8944 line 370
  77. def OAI.MUB6.Certificate.PairSemantics.raw8945 line 388
  78. def OAI.MUB6.Certificate.PairSemantics.raw8945step0 line 390
  79. def OAI.MUB6.Certificate.PairSemantics.raw8945step1 line 392
  80. def OAI.MUB6.Certificate.PairSemantics.raw8945step2 line 394
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical8945 line 396
  82. def OAI.MUB6.Certificate.PairSemantics.raw8946 line 414
  83. def OAI.MUB6.Certificate.PairSemantics.raw8946step0 line 416
  84. def OAI.MUB6.Certificate.PairSemantics.raw8946step1 line 418
  85. def OAI.MUB6.Certificate.PairSemantics.raw8946step2 line 420
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical8946 line 422
  87. def OAI.MUB6.Certificate.PairSemantics.raw8947 line 442
  88. def OAI.MUB6.Certificate.PairSemantics.raw8947step0 line 444
  89. def OAI.MUB6.Certificate.PairSemantics.raw8947step1 line 446
  90. def OAI.MUB6.Certificate.PairSemantics.raw8947step2 line 448
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical8947 line 450
  92. def OAI.MUB6.Certificate.PairSemantics.raw8948 line 470
  93. def OAI.MUB6.Certificate.PairSemantics.raw8948step0 line 472
  94. def OAI.MUB6.Certificate.PairSemantics.raw8948step1 line 474
  95. def OAI.MUB6.Certificate.PairSemantics.raw8948step2 line 476
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical8948 line 478
  97. def OAI.MUB6.Certificate.PairSemantics.raw8949 line 497
  98. def OAI.MUB6.Certificate.PairSemantics.raw8949step0 line 499
  99. def OAI.MUB6.Certificate.PairSemantics.raw8949step1 line 501
  100. def OAI.MUB6.Certificate.PairSemantics.raw8949step2 line 503
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical8949 line 505
  102. def OAI.MUB6.Certificate.PairSemantics.raw8950 line 525
  103. def OAI.MUB6.Certificate.PairSemantics.raw8950step0 line 527
  104. def OAI.MUB6.Certificate.PairSemantics.raw8950step1 line 529
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical8950 line 531
  106. def OAI.MUB6.Certificate.PairSemantics.raw8951 line 546
  107. def OAI.MUB6.Certificate.PairSemantics.raw8951step0 line 548
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical8951 line 550
  109. def OAI.MUB6.Certificate.PairSemantics.raw8952 line 560
  110. def OAI.MUB6.Certificate.PairSemantics.raw8952step0 line 562
  111. def OAI.MUB6.Certificate.PairSemantics.raw8952step1 line 564
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical8952 line 566
  113. def OAI.MUB6.Certificate.PairSemantics.raw8953 line 581
  114. def OAI.MUB6.Certificate.PairSemantics.raw8953step0 line 583
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical8953 line 585
  116. def OAI.MUB6.Certificate.PairSemantics.raw8954 line 595
  117. def OAI.MUB6.Certificate.PairSemantics.raw8954step0 line 597
  118. def OAI.MUB6.Certificate.PairSemantics.raw8954step1 line 599
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical8954 line 601
  120. def OAI.MUB6.Certificate.PairSemantics.raw8955 line 616
  121. def OAI.MUB6.Certificate.PairSemantics.raw8955step0 line 618
  122. def OAI.MUB6.Certificate.PairSemantics.raw8955step1 line 620
  123. theorem OAI.MUB6.Certificate.PairSemantics.canonical8955 line 622
  124. def OAI.MUB6.Certificate.PairSemantics.raw8956 line 636
  125. def OAI.MUB6.Certificate.PairSemantics.raw8956step0 line 638
  126. theorem OAI.MUB6.Certificate.PairSemantics.canonical8956 line 640
  127. def OAI.MUB6.Certificate.PairSemantics.raw8957 line 650
  128. def OAI.MUB6.Certificate.PairSemantics.raw8957step0 line 652
  129. def OAI.MUB6.Certificate.PairSemantics.raw8957step1 line 654
  130. def OAI.MUB6.Certificate.PairSemantics.raw8957step2 line 656
  131. def OAI.MUB6.Certificate.PairSemantics.raw8957step3 line 658
  132. theorem OAI.MUB6.Certificate.PairSemantics.canonical8957 line 660
  133. def OAI.MUB6.Certificate.PairSemantics.raw8958 line 684
  134. def OAI.MUB6.Certificate.PairSemantics.raw8958step0 line 686
  135. def OAI.MUB6.Certificate.PairSemantics.raw8958step1 line 688
  136. def OAI.MUB6.Certificate.PairSemantics.raw8958step2 line 690
  137. theorem OAI.MUB6.Certificate.PairSemantics.canonical8958 line 692
  138. def OAI.MUB6.Certificate.PairSemantics.raw8959 line 711
  139. def OAI.MUB6.Certificate.PairSemantics.raw8959step0 line 713
  140. def OAI.MUB6.Certificate.PairSemantics.raw8959step1 line 715
  141. def OAI.MUB6.Certificate.PairSemantics.raw8959step2 line 717
  142. theorem OAI.MUB6.Certificate.PairSemantics.canonical8959 line 719