OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical248.lean

GitHub source file

139 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7936 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw7936step0 line 20
  3. def OAI.MUB6.Certificate.PairSemantics.raw7936step1 line 22
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7936 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw7937 line 37
  6. def OAI.MUB6.Certificate.PairSemantics.raw7937step0 line 39
  7. def OAI.MUB6.Certificate.PairSemantics.raw7937step1 line 41
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical7937 line 43
  9. def OAI.MUB6.Certificate.PairSemantics.raw7938 line 56
  10. def OAI.MUB6.Certificate.PairSemantics.raw7938step0 line 58
  11. def OAI.MUB6.Certificate.PairSemantics.raw7938step1 line 60
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical7938 line 62
  13. def OAI.MUB6.Certificate.PairSemantics.raw7939 line 75
  14. def OAI.MUB6.Certificate.PairSemantics.raw7939step0 line 77
  15. def OAI.MUB6.Certificate.PairSemantics.raw7939step1 line 79
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical7939 line 81
  17. def OAI.MUB6.Certificate.PairSemantics.raw7940 line 94
  18. def OAI.MUB6.Certificate.PairSemantics.raw7940step0 line 96
  19. def OAI.MUB6.Certificate.PairSemantics.raw7940step1 line 98
  20. def OAI.MUB6.Certificate.PairSemantics.raw7940step2 line 100
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical7940 line 102
  22. def OAI.MUB6.Certificate.PairSemantics.raw7941 line 119
  23. def OAI.MUB6.Certificate.PairSemantics.raw7941step0 line 121
  24. def OAI.MUB6.Certificate.PairSemantics.raw7941step1 line 123
  25. def OAI.MUB6.Certificate.PairSemantics.raw7941step2 line 125
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical7941 line 127
  27. def OAI.MUB6.Certificate.PairSemantics.raw7942 line 144
  28. def OAI.MUB6.Certificate.PairSemantics.raw7942step0 line 146
  29. def OAI.MUB6.Certificate.PairSemantics.raw7942step1 line 148
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical7942 line 150
  31. def OAI.MUB6.Certificate.PairSemantics.raw7943 line 163
  32. def OAI.MUB6.Certificate.PairSemantics.raw7943step0 line 165
  33. def OAI.MUB6.Certificate.PairSemantics.raw7943step1 line 167
  34. def OAI.MUB6.Certificate.PairSemantics.raw7943step2 line 169
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical7943 line 171
  36. def OAI.MUB6.Certificate.PairSemantics.raw7944 line 188
  37. def OAI.MUB6.Certificate.PairSemantics.raw7944step0 line 190
  38. def OAI.MUB6.Certificate.PairSemantics.raw7944step1 line 192
  39. def OAI.MUB6.Certificate.PairSemantics.raw7944step2 line 194
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical7944 line 196
  41. def OAI.MUB6.Certificate.PairSemantics.raw7945 line 213
  42. def OAI.MUB6.Certificate.PairSemantics.raw7945step0 line 215
  43. def OAI.MUB6.Certificate.PairSemantics.raw7945step1 line 217
  44. def OAI.MUB6.Certificate.PairSemantics.raw7945step2 line 219
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical7945 line 221
  46. def OAI.MUB6.Certificate.PairSemantics.raw7946 line 238
  47. def OAI.MUB6.Certificate.PairSemantics.raw7946step0 line 240
  48. def OAI.MUB6.Certificate.PairSemantics.raw7946step1 line 242
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical7946 line 244
  50. def OAI.MUB6.Certificate.PairSemantics.raw7947 line 257
  51. def OAI.MUB6.Certificate.PairSemantics.raw7947step0 line 259
  52. def OAI.MUB6.Certificate.PairSemantics.raw7947step1 line 261
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical7947 line 263
  54. def OAI.MUB6.Certificate.PairSemantics.raw7948 line 276
  55. def OAI.MUB6.Certificate.PairSemantics.raw7948step0 line 278
  56. def OAI.MUB6.Certificate.PairSemantics.raw7948step1 line 280
  57. def OAI.MUB6.Certificate.PairSemantics.raw7948step2 line 282
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical7948 line 284
  59. def OAI.MUB6.Certificate.PairSemantics.raw7949 line 301
  60. def OAI.MUB6.Certificate.PairSemantics.raw7949step0 line 303
  61. def OAI.MUB6.Certificate.PairSemantics.raw7949step1 line 305
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical7949 line 307
  63. def OAI.MUB6.Certificate.PairSemantics.raw7950 line 320
  64. def OAI.MUB6.Certificate.PairSemantics.raw7950step0 line 322
  65. def OAI.MUB6.Certificate.PairSemantics.raw7950step1 line 324
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical7950 line 326
  67. def OAI.MUB6.Certificate.PairSemantics.raw7951 line 339
  68. def OAI.MUB6.Certificate.PairSemantics.raw7951step0 line 341
  69. def OAI.MUB6.Certificate.PairSemantics.raw7951step1 line 343
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical7951 line 345
  71. def OAI.MUB6.Certificate.PairSemantics.raw7952 line 358
  72. def OAI.MUB6.Certificate.PairSemantics.raw7952step0 line 360
  73. def OAI.MUB6.Certificate.PairSemantics.raw7952step1 line 362
  74. def OAI.MUB6.Certificate.PairSemantics.raw7952step2 line 364
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical7952 line 366
  76. def OAI.MUB6.Certificate.PairSemantics.raw7953 line 383
  77. def OAI.MUB6.Certificate.PairSemantics.raw7953step0 line 385
  78. def OAI.MUB6.Certificate.PairSemantics.raw7953step1 line 387
  79. def OAI.MUB6.Certificate.PairSemantics.raw7953step2 line 389
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical7953 line 391
  81. def OAI.MUB6.Certificate.PairSemantics.raw7954 line 408
  82. def OAI.MUB6.Certificate.PairSemantics.raw7954step0 line 410
  83. def OAI.MUB6.Certificate.PairSemantics.raw7954step1 line 412
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical7954 line 414
  85. def OAI.MUB6.Certificate.PairSemantics.raw7955 line 427
  86. def OAI.MUB6.Certificate.PairSemantics.raw7955step0 line 429
  87. def OAI.MUB6.Certificate.PairSemantics.raw7955step1 line 431
  88. def OAI.MUB6.Certificate.PairSemantics.raw7955step2 line 433
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical7955 line 435
  90. def OAI.MUB6.Certificate.PairSemantics.raw7956 line 452
  91. def OAI.MUB6.Certificate.PairSemantics.raw7956step0 line 454
  92. def OAI.MUB6.Certificate.PairSemantics.raw7956step1 line 456
  93. def OAI.MUB6.Certificate.PairSemantics.raw7956step2 line 458
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical7956 line 460
  95. def OAI.MUB6.Certificate.PairSemantics.raw7957 line 477
  96. def OAI.MUB6.Certificate.PairSemantics.raw7957step0 line 479
  97. def OAI.MUB6.Certificate.PairSemantics.raw7957step1 line 481
  98. def OAI.MUB6.Certificate.PairSemantics.raw7957step2 line 483
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical7957 line 485
  100. def OAI.MUB6.Certificate.PairSemantics.raw7958 line 502
  101. def OAI.MUB6.Certificate.PairSemantics.raw7958step0 line 504
  102. def OAI.MUB6.Certificate.PairSemantics.raw7958step1 line 506
  103. def OAI.MUB6.Certificate.PairSemantics.raw7958step2 line 508
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical7958 line 510
  105. def OAI.MUB6.Certificate.PairSemantics.raw7959 line 527
  106. def OAI.MUB6.Certificate.PairSemantics.raw7959step0 line 529
  107. def OAI.MUB6.Certificate.PairSemantics.raw7959step1 line 531
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical7959 line 533
  109. def OAI.MUB6.Certificate.PairSemantics.raw7960 line 546
  110. def OAI.MUB6.Certificate.PairSemantics.raw7960step0 line 548
  111. def OAI.MUB6.Certificate.PairSemantics.raw7960step1 line 550
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical7960 line 552
  113. def OAI.MUB6.Certificate.PairSemantics.raw7961 line 565
  114. def OAI.MUB6.Certificate.PairSemantics.raw7961step0 line 567
  115. def OAI.MUB6.Certificate.PairSemantics.raw7961step1 line 569
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical7961 line 571
  117. def OAI.MUB6.Certificate.PairSemantics.raw7962 line 584
  118. def OAI.MUB6.Certificate.PairSemantics.raw7962step0 line 586
  119. def OAI.MUB6.Certificate.PairSemantics.raw7962step1 line 588
  120. def OAI.MUB6.Certificate.PairSemantics.raw7962step2 line 590
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical7962 line 592
  122. def OAI.MUB6.Certificate.PairSemantics.raw7963 line 609
  123. def OAI.MUB6.Certificate.PairSemantics.raw7963step0 line 611
  124. def OAI.MUB6.Certificate.PairSemantics.raw7963step1 line 613
  125. def OAI.MUB6.Certificate.PairSemantics.raw7963step2 line 615
  126. theorem OAI.MUB6.Certificate.PairSemantics.canonical7963 line 617
  127. def OAI.MUB6.Certificate.PairSemantics.raw7964 line 634
  128. def OAI.MUB6.Certificate.PairSemantics.raw7964step0 line 636
  129. def OAI.MUB6.Certificate.PairSemantics.raw7964step1 line 638
  130. theorem OAI.MUB6.Certificate.PairSemantics.canonical7964 line 640
  131. def OAI.MUB6.Certificate.PairSemantics.raw7965 line 653
  132. theorem OAI.MUB6.Certificate.PairSemantics.canonical7965 line 655
  133. def OAI.MUB6.Certificate.PairSemantics.raw7966 line 659
  134. def OAI.MUB6.Certificate.PairSemantics.raw7966step0 line 661
  135. theorem OAI.MUB6.Certificate.PairSemantics.canonical7966 line 663
  136. def OAI.MUB6.Certificate.PairSemantics.raw7967 line 672
  137. def OAI.MUB6.Certificate.PairSemantics.raw7967step0 line 674
  138. def OAI.MUB6.Certificate.PairSemantics.raw7967step1 line 676
  139. theorem OAI.MUB6.Certificate.PairSemantics.canonical7967 line 678