OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical241.lean

GitHub source file

125 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7712 line 12
  2. def OAI.MUB6.Certificate.PairSemantics.raw7712step0 line 14
  3. def OAI.MUB6.Certificate.PairSemantics.raw7712step1 line 16
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7712 line 18
  5. def OAI.MUB6.Certificate.PairSemantics.raw7713 line 32
  6. def OAI.MUB6.Certificate.PairSemantics.raw7713step0 line 34
  7. def OAI.MUB6.Certificate.PairSemantics.raw7713step1 line 36
  8. def OAI.MUB6.Certificate.PairSemantics.raw7713step2 line 38
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical7713 line 40
  10. def OAI.MUB6.Certificate.PairSemantics.raw7714 line 60
  11. def OAI.MUB6.Certificate.PairSemantics.raw7714step0 line 62
  12. def OAI.MUB6.Certificate.PairSemantics.raw7714step1 line 64
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical7714 line 66
  14. def OAI.MUB6.Certificate.PairSemantics.raw7715 line 80
  15. def OAI.MUB6.Certificate.PairSemantics.raw7715step0 line 82
  16. def OAI.MUB6.Certificate.PairSemantics.raw7715step1 line 84
  17. def OAI.MUB6.Certificate.PairSemantics.raw7715step2 line 86
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical7715 line 88
  19. def OAI.MUB6.Certificate.PairSemantics.raw7716 line 107
  20. def OAI.MUB6.Certificate.PairSemantics.raw7716step0 line 109
  21. def OAI.MUB6.Certificate.PairSemantics.raw7716step1 line 111
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical7716 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw7717 line 127
  24. def OAI.MUB6.Certificate.PairSemantics.raw7717step0 line 129
  25. def OAI.MUB6.Certificate.PairSemantics.raw7717step1 line 131
  26. def OAI.MUB6.Certificate.PairSemantics.raw7717step2 line 133
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical7717 line 135
  28. def OAI.MUB6.Certificate.PairSemantics.raw7718 line 154
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical7718 line 156
  30. def OAI.MUB6.Certificate.PairSemantics.raw7719 line 160
  31. def OAI.MUB6.Certificate.PairSemantics.raw7719step0 line 162
  32. def OAI.MUB6.Certificate.PairSemantics.raw7719step1 line 164
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical7719 line 166
  34. def OAI.MUB6.Certificate.PairSemantics.raw7720 line 180
  35. def OAI.MUB6.Certificate.PairSemantics.raw7720step0 line 182
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical7720 line 184
  37. def OAI.MUB6.Certificate.PairSemantics.raw7721 line 193
  38. def OAI.MUB6.Certificate.PairSemantics.raw7721step0 line 195
  39. def OAI.MUB6.Certificate.PairSemantics.raw7721step1 line 197
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical7721 line 199
  41. def OAI.MUB6.Certificate.PairSemantics.raw7722 line 213
  42. def OAI.MUB6.Certificate.PairSemantics.raw7722step0 line 215
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical7722 line 217
  44. def OAI.MUB6.Certificate.PairSemantics.raw7723 line 226
  45. def OAI.MUB6.Certificate.PairSemantics.raw7723step0 line 228
  46. def OAI.MUB6.Certificate.PairSemantics.raw7723step1 line 230
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical7723 line 232
  48. def OAI.MUB6.Certificate.PairSemantics.raw7724 line 246
  49. def OAI.MUB6.Certificate.PairSemantics.raw7724step0 line 248
  50. def OAI.MUB6.Certificate.PairSemantics.raw7724step1 line 250
  51. def OAI.MUB6.Certificate.PairSemantics.raw7724step2 line 252
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical7724 line 254
  53. def OAI.MUB6.Certificate.PairSemantics.raw7725 line 273
  54. def OAI.MUB6.Certificate.PairSemantics.raw7725step0 line 275
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical7725 line 277
  56. def OAI.MUB6.Certificate.PairSemantics.raw7726 line 286
  57. def OAI.MUB6.Certificate.PairSemantics.raw7726step0 line 288
  58. def OAI.MUB6.Certificate.PairSemantics.raw7726step1 line 290
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical7726 line 292
  60. def OAI.MUB6.Certificate.PairSemantics.raw7727 line 306
  61. def OAI.MUB6.Certificate.PairSemantics.raw7727step0 line 308
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical7727 line 310
  63. def OAI.MUB6.Certificate.PairSemantics.raw7728 line 319
  64. def OAI.MUB6.Certificate.PairSemantics.raw7728step0 line 321
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical7728 line 323
  66. def OAI.MUB6.Certificate.PairSemantics.raw7729 line 332
  67. def OAI.MUB6.Certificate.PairSemantics.raw7729step0 line 334
  68. def OAI.MUB6.Certificate.PairSemantics.raw7729step1 line 336
  69. def OAI.MUB6.Certificate.PairSemantics.raw7729step2 line 338
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical7729 line 340
  71. def OAI.MUB6.Certificate.PairSemantics.raw7730 line 359
  72. def OAI.MUB6.Certificate.PairSemantics.raw7730step0 line 361
  73. def OAI.MUB6.Certificate.PairSemantics.raw7730step1 line 363
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical7730 line 365
  75. def OAI.MUB6.Certificate.PairSemantics.raw7731 line 379
  76. def OAI.MUB6.Certificate.PairSemantics.raw7731step0 line 381
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical7731 line 383
  78. def OAI.MUB6.Certificate.PairSemantics.raw7732 line 392
  79. def OAI.MUB6.Certificate.PairSemantics.raw7732step0 line 394
  80. def OAI.MUB6.Certificate.PairSemantics.raw7732step1 line 396
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical7732 line 398
  82. def OAI.MUB6.Certificate.PairSemantics.raw7733 line 412
  83. def OAI.MUB6.Certificate.PairSemantics.raw7733step0 line 414
  84. def OAI.MUB6.Certificate.PairSemantics.raw7733step1 line 416
  85. def OAI.MUB6.Certificate.PairSemantics.raw7733step2 line 418
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical7733 line 420
  87. def OAI.MUB6.Certificate.PairSemantics.raw7734 line 439
  88. def OAI.MUB6.Certificate.PairSemantics.raw7734step0 line 441
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical7734 line 443
  90. def OAI.MUB6.Certificate.PairSemantics.raw7735 line 452
  91. def OAI.MUB6.Certificate.PairSemantics.raw7735step0 line 454
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical7735 line 456
  93. def OAI.MUB6.Certificate.PairSemantics.raw7736 line 466
  94. def OAI.MUB6.Certificate.PairSemantics.raw7736step0 line 468
  95. def OAI.MUB6.Certificate.PairSemantics.raw7736step1 line 470
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical7736 line 472
  97. def OAI.MUB6.Certificate.PairSemantics.raw7737 line 487
  98. def OAI.MUB6.Certificate.PairSemantics.raw7737step0 line 489
  99. def OAI.MUB6.Certificate.PairSemantics.raw7737step1 line 491
  100. def OAI.MUB6.Certificate.PairSemantics.raw7737step2 line 493
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical7737 line 495
  102. def OAI.MUB6.Certificate.PairSemantics.raw7738 line 515
  103. def OAI.MUB6.Certificate.PairSemantics.raw7738step0 line 517
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical7738 line 519
  105. def OAI.MUB6.Certificate.PairSemantics.raw7739 line 528
  106. def OAI.MUB6.Certificate.PairSemantics.raw7739step0 line 530
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical7739 line 532
  108. def OAI.MUB6.Certificate.PairSemantics.raw7740 line 541
  109. def OAI.MUB6.Certificate.PairSemantics.raw7740step0 line 543
  110. def OAI.MUB6.Certificate.PairSemantics.raw7740step1 line 545
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical7740 line 547
  112. def OAI.MUB6.Certificate.PairSemantics.raw7741 line 561
  113. def OAI.MUB6.Certificate.PairSemantics.raw7741step0 line 563
  114. def OAI.MUB6.Certificate.PairSemantics.raw7741step1 line 565
  115. def OAI.MUB6.Certificate.PairSemantics.raw7741step2 line 567
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical7741 line 569
  117. def OAI.MUB6.Certificate.PairSemantics.raw7742 line 588
  118. def OAI.MUB6.Certificate.PairSemantics.raw7742step0 line 590
  119. def OAI.MUB6.Certificate.PairSemantics.raw7742step1 line 592
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical7742 line 594
  121. def OAI.MUB6.Certificate.PairSemantics.raw7743 line 608
  122. def OAI.MUB6.Certificate.PairSemantics.raw7743step0 line 610
  123. def OAI.MUB6.Certificate.PairSemantics.raw7743step1 line 612
  124. def OAI.MUB6.Certificate.PairSemantics.raw7743step2 line 614
  125. theorem OAI.MUB6.Certificate.PairSemantics.canonical7743 line 616