OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical234.lean

GitHub source file

139 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7488 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw7488step0 line 23
  3. def OAI.MUB6.Certificate.PairSemantics.raw7488step1 line 25
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7488 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw7489 line 40
  6. def OAI.MUB6.Certificate.PairSemantics.raw7489step0 line 42
  7. def OAI.MUB6.Certificate.PairSemantics.raw7489step1 line 44
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical7489 line 46
  9. def OAI.MUB6.Certificate.PairSemantics.raw7490 line 59
  10. def OAI.MUB6.Certificate.PairSemantics.raw7490step0 line 61
  11. def OAI.MUB6.Certificate.PairSemantics.raw7490step1 line 63
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical7490 line 65
  13. def OAI.MUB6.Certificate.PairSemantics.raw7491 line 78
  14. def OAI.MUB6.Certificate.PairSemantics.raw7491step0 line 80
  15. def OAI.MUB6.Certificate.PairSemantics.raw7491step1 line 82
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical7491 line 84
  17. def OAI.MUB6.Certificate.PairSemantics.raw7492 line 97
  18. def OAI.MUB6.Certificate.PairSemantics.raw7492step0 line 99
  19. def OAI.MUB6.Certificate.PairSemantics.raw7492step1 line 101
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical7492 line 103
  21. def OAI.MUB6.Certificate.PairSemantics.raw7493 line 116
  22. def OAI.MUB6.Certificate.PairSemantics.raw7493step0 line 118
  23. def OAI.MUB6.Certificate.PairSemantics.raw7493step1 line 120
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical7493 line 122
  25. def OAI.MUB6.Certificate.PairSemantics.raw7494 line 135
  26. def OAI.MUB6.Certificate.PairSemantics.raw7494step0 line 137
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical7494 line 139
  28. def OAI.MUB6.Certificate.PairSemantics.raw7495 line 148
  29. def OAI.MUB6.Certificate.PairSemantics.raw7495step0 line 150
  30. def OAI.MUB6.Certificate.PairSemantics.raw7495step1 line 152
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical7495 line 154
  32. def OAI.MUB6.Certificate.PairSemantics.raw7496 line 167
  33. def OAI.MUB6.Certificate.PairSemantics.raw7496step0 line 169
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical7496 line 171
  35. def OAI.MUB6.Certificate.PairSemantics.raw7497 line 180
  36. def OAI.MUB6.Certificate.PairSemantics.raw7497step0 line 182
  37. def OAI.MUB6.Certificate.PairSemantics.raw7497step1 line 184
  38. def OAI.MUB6.Certificate.PairSemantics.raw7497step2 line 186
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical7497 line 188
  40. def OAI.MUB6.Certificate.PairSemantics.raw7498 line 206
  41. def OAI.MUB6.Certificate.PairSemantics.raw7498step0 line 208
  42. def OAI.MUB6.Certificate.PairSemantics.raw7498step1 line 210
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical7498 line 212
  44. def OAI.MUB6.Certificate.PairSemantics.raw7499 line 225
  45. def OAI.MUB6.Certificate.PairSemantics.raw7499step0 line 227
  46. def OAI.MUB6.Certificate.PairSemantics.raw7499step1 line 229
  47. def OAI.MUB6.Certificate.PairSemantics.raw7499step2 line 231
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical7499 line 233
  49. def OAI.MUB6.Certificate.PairSemantics.raw7500 line 251
  50. def OAI.MUB6.Certificate.PairSemantics.raw7500step0 line 253
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical7500 line 255
  52. def OAI.MUB6.Certificate.PairSemantics.raw7501 line 264
  53. def OAI.MUB6.Certificate.PairSemantics.raw7501step0 line 266
  54. def OAI.MUB6.Certificate.PairSemantics.raw7501step1 line 268
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical7501 line 270
  56. def OAI.MUB6.Certificate.PairSemantics.raw7502 line 283
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical7502 line 285
  58. def OAI.MUB6.Certificate.PairSemantics.raw7503 line 289
  59. def OAI.MUB6.Certificate.PairSemantics.raw7503step0 line 291
  60. def OAI.MUB6.Certificate.PairSemantics.raw7503step1 line 293
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical7503 line 295
  62. def OAI.MUB6.Certificate.PairSemantics.raw7504 line 308
  63. def OAI.MUB6.Certificate.PairSemantics.raw7504step0 line 310
  64. def OAI.MUB6.Certificate.PairSemantics.raw7504step1 line 312
  65. def OAI.MUB6.Certificate.PairSemantics.raw7504step2 line 314
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical7504 line 316
  67. def OAI.MUB6.Certificate.PairSemantics.raw7505 line 333
  68. def OAI.MUB6.Certificate.PairSemantics.raw7505step0 line 335
  69. def OAI.MUB6.Certificate.PairSemantics.raw7505step1 line 337
  70. def OAI.MUB6.Certificate.PairSemantics.raw7505step2 line 339
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical7505 line 341
  72. def OAI.MUB6.Certificate.PairSemantics.raw7506 line 358
  73. def OAI.MUB6.Certificate.PairSemantics.raw7506step0 line 360
  74. def OAI.MUB6.Certificate.PairSemantics.raw7506step1 line 362
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical7506 line 364
  76. def OAI.MUB6.Certificate.PairSemantics.raw7507 line 377
  77. def OAI.MUB6.Certificate.PairSemantics.raw7507step0 line 379
  78. def OAI.MUB6.Certificate.PairSemantics.raw7507step1 line 381
  79. def OAI.MUB6.Certificate.PairSemantics.raw7507step2 line 383
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical7507 line 385
  81. def OAI.MUB6.Certificate.PairSemantics.raw7508 line 402
  82. def OAI.MUB6.Certificate.PairSemantics.raw7508step0 line 404
  83. def OAI.MUB6.Certificate.PairSemantics.raw7508step1 line 406
  84. def OAI.MUB6.Certificate.PairSemantics.raw7508step2 line 408
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical7508 line 410
  86. def OAI.MUB6.Certificate.PairSemantics.raw7509 line 427
  87. def OAI.MUB6.Certificate.PairSemantics.raw7509step0 line 429
  88. def OAI.MUB6.Certificate.PairSemantics.raw7509step1 line 431
  89. def OAI.MUB6.Certificate.PairSemantics.raw7509step2 line 433
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical7509 line 435
  91. def OAI.MUB6.Certificate.PairSemantics.raw7510 line 452
  92. def OAI.MUB6.Certificate.PairSemantics.raw7510step0 line 454
  93. def OAI.MUB6.Certificate.PairSemantics.raw7510step1 line 456
  94. def OAI.MUB6.Certificate.PairSemantics.raw7510step2 line 458
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical7510 line 460
  96. def OAI.MUB6.Certificate.PairSemantics.raw7511 line 477
  97. def OAI.MUB6.Certificate.PairSemantics.raw7511step0 line 479
  98. def OAI.MUB6.Certificate.PairSemantics.raw7511step1 line 481
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical7511 line 483
  100. def OAI.MUB6.Certificate.PairSemantics.raw7512 line 496
  101. def OAI.MUB6.Certificate.PairSemantics.raw7512step0 line 498
  102. def OAI.MUB6.Certificate.PairSemantics.raw7512step1 line 500
  103. def OAI.MUB6.Certificate.PairSemantics.raw7512step2 line 502
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical7512 line 504
  105. def OAI.MUB6.Certificate.PairSemantics.raw7513 line 521
  106. def OAI.MUB6.Certificate.PairSemantics.raw7513step0 line 523
  107. def OAI.MUB6.Certificate.PairSemantics.raw7513step1 line 525
  108. def OAI.MUB6.Certificate.PairSemantics.raw7513step2 line 527
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical7513 line 529
  110. def OAI.MUB6.Certificate.PairSemantics.raw7514 line 546
  111. def OAI.MUB6.Certificate.PairSemantics.raw7514step0 line 548
  112. def OAI.MUB6.Certificate.PairSemantics.raw7514step1 line 550
  113. def OAI.MUB6.Certificate.PairSemantics.raw7514step2 line 552
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical7514 line 554
  115. def OAI.MUB6.Certificate.PairSemantics.raw7515 line 571
  116. def OAI.MUB6.Certificate.PairSemantics.raw7515step0 line 573
  117. def OAI.MUB6.Certificate.PairSemantics.raw7515step1 line 575
  118. def OAI.MUB6.Certificate.PairSemantics.raw7515step2 line 577
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical7515 line 579
  120. def OAI.MUB6.Certificate.PairSemantics.raw7516 line 596
  121. def OAI.MUB6.Certificate.PairSemantics.raw7516step0 line 598
  122. def OAI.MUB6.Certificate.PairSemantics.raw7516step1 line 600
  123. def OAI.MUB6.Certificate.PairSemantics.raw7516step2 line 602
  124. theorem OAI.MUB6.Certificate.PairSemantics.canonical7516 line 604
  125. def OAI.MUB6.Certificate.PairSemantics.raw7517 line 621
  126. def OAI.MUB6.Certificate.PairSemantics.raw7517step0 line 623
  127. def OAI.MUB6.Certificate.PairSemantics.raw7517step1 line 625
  128. def OAI.MUB6.Certificate.PairSemantics.raw7517step2 line 627
  129. theorem OAI.MUB6.Certificate.PairSemantics.canonical7517 line 629
  130. def OAI.MUB6.Certificate.PairSemantics.raw7518 line 646
  131. def OAI.MUB6.Certificate.PairSemantics.raw7518step0 line 648
  132. def OAI.MUB6.Certificate.PairSemantics.raw7518step1 line 650
  133. def OAI.MUB6.Certificate.PairSemantics.raw7518step2 line 652
  134. theorem OAI.MUB6.Certificate.PairSemantics.canonical7518 line 654
  135. def OAI.MUB6.Certificate.PairSemantics.raw7519 line 671
  136. def OAI.MUB6.Certificate.PairSemantics.raw7519step0 line 673
  137. def OAI.MUB6.Certificate.PairSemantics.raw7519step1 line 675
  138. def OAI.MUB6.Certificate.PairSemantics.raw7519step2 line 677
  139. theorem OAI.MUB6.Certificate.PairSemantics.canonical7519 line 679