OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical209.lean

GitHub source file

129 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6688 line 12
  2. def OAI.MUB6.Certificate.PairSemantics.raw6688step0 line 14
  3. def OAI.MUB6.Certificate.PairSemantics.raw6688step1 line 16
  4. def OAI.MUB6.Certificate.PairSemantics.raw6688step2 line 18
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical6688 line 20
  6. def OAI.MUB6.Certificate.PairSemantics.raw6689 line 37
  7. def OAI.MUB6.Certificate.PairSemantics.raw6689step0 line 39
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical6689 line 41
  9. def OAI.MUB6.Certificate.PairSemantics.raw6690 line 50
  10. def OAI.MUB6.Certificate.PairSemantics.raw6690step0 line 52
  11. def OAI.MUB6.Certificate.PairSemantics.raw6690step1 line 54
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical6690 line 56
  13. def OAI.MUB6.Certificate.PairSemantics.raw6691 line 69
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical6691 line 71
  15. def OAI.MUB6.Certificate.PairSemantics.raw6692 line 75
  16. def OAI.MUB6.Certificate.PairSemantics.raw6692step0 line 77
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical6692 line 79
  18. def OAI.MUB6.Certificate.PairSemantics.raw6693 line 88
  19. def OAI.MUB6.Certificate.PairSemantics.raw6693step0 line 90
  20. def OAI.MUB6.Certificate.PairSemantics.raw6693step1 line 92
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical6693 line 94
  22. def OAI.MUB6.Certificate.PairSemantics.raw6694 line 107
  23. def OAI.MUB6.Certificate.PairSemantics.raw6694step0 line 109
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical6694 line 111
  25. def OAI.MUB6.Certificate.PairSemantics.raw6695 line 120
  26. def OAI.MUB6.Certificate.PairSemantics.raw6695step0 line 122
  27. def OAI.MUB6.Certificate.PairSemantics.raw6695step1 line 124
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical6695 line 126
  29. def OAI.MUB6.Certificate.PairSemantics.raw6696 line 139
  30. def OAI.MUB6.Certificate.PairSemantics.raw6696step0 line 141
  31. def OAI.MUB6.Certificate.PairSemantics.raw6696step1 line 143
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical6696 line 145
  33. def OAI.MUB6.Certificate.PairSemantics.raw6697 line 158
  34. def OAI.MUB6.Certificate.PairSemantics.raw6697step0 line 160
  35. def OAI.MUB6.Certificate.PairSemantics.raw6697step1 line 162
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical6697 line 164
  37. def OAI.MUB6.Certificate.PairSemantics.raw6698 line 177
  38. def OAI.MUB6.Certificate.PairSemantics.raw6698step0 line 179
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical6698 line 181
  40. def OAI.MUB6.Certificate.PairSemantics.raw6699 line 190
  41. def OAI.MUB6.Certificate.PairSemantics.raw6699step0 line 192
  42. def OAI.MUB6.Certificate.PairSemantics.raw6699step1 line 194
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical6699 line 196
  44. def OAI.MUB6.Certificate.PairSemantics.raw6700 line 209
  45. def OAI.MUB6.Certificate.PairSemantics.raw6700step0 line 211
  46. def OAI.MUB6.Certificate.PairSemantics.raw6700step1 line 213
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical6700 line 215
  48. def OAI.MUB6.Certificate.PairSemantics.raw6701 line 228
  49. def OAI.MUB6.Certificate.PairSemantics.raw6701step0 line 230
  50. def OAI.MUB6.Certificate.PairSemantics.raw6701step1 line 232
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical6701 line 234
  52. def OAI.MUB6.Certificate.PairSemantics.raw6702 line 247
  53. def OAI.MUB6.Certificate.PairSemantics.raw6702step0 line 249
  54. def OAI.MUB6.Certificate.PairSemantics.raw6702step1 line 251
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical6702 line 253
  56. def OAI.MUB6.Certificate.PairSemantics.raw6703 line 266
  57. def OAI.MUB6.Certificate.PairSemantics.raw6703step0 line 268
  58. def OAI.MUB6.Certificate.PairSemantics.raw6703step1 line 270
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical6703 line 272
  60. def OAI.MUB6.Certificate.PairSemantics.raw6704 line 285
  61. def OAI.MUB6.Certificate.PairSemantics.raw6704step0 line 287
  62. def OAI.MUB6.Certificate.PairSemantics.raw6704step1 line 289
  63. def OAI.MUB6.Certificate.PairSemantics.raw6704step2 line 291
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical6704 line 293
  65. def OAI.MUB6.Certificate.PairSemantics.raw6705 line 310
  66. def OAI.MUB6.Certificate.PairSemantics.raw6705step0 line 312
  67. def OAI.MUB6.Certificate.PairSemantics.raw6705step1 line 314
  68. def OAI.MUB6.Certificate.PairSemantics.raw6705step2 line 316
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical6705 line 318
  70. def OAI.MUB6.Certificate.PairSemantics.raw6706 line 335
  71. def OAI.MUB6.Certificate.PairSemantics.raw6706step0 line 337
  72. def OAI.MUB6.Certificate.PairSemantics.raw6706step1 line 339
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical6706 line 341
  74. def OAI.MUB6.Certificate.PairSemantics.raw6707 line 354
  75. def OAI.MUB6.Certificate.PairSemantics.raw6707step0 line 356
  76. def OAI.MUB6.Certificate.PairSemantics.raw6707step1 line 358
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical6707 line 360
  78. def OAI.MUB6.Certificate.PairSemantics.raw6708 line 373
  79. def OAI.MUB6.Certificate.PairSemantics.raw6708step0 line 375
  80. def OAI.MUB6.Certificate.PairSemantics.raw6708step1 line 377
  81. def OAI.MUB6.Certificate.PairSemantics.raw6708step2 line 379
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical6708 line 381
  83. def OAI.MUB6.Certificate.PairSemantics.raw6709 line 398
  84. def OAI.MUB6.Certificate.PairSemantics.raw6709step0 line 400
  85. def OAI.MUB6.Certificate.PairSemantics.raw6709step1 line 402
  86. def OAI.MUB6.Certificate.PairSemantics.raw6709step2 line 404
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical6709 line 406
  88. def OAI.MUB6.Certificate.PairSemantics.raw6710 line 423
  89. def OAI.MUB6.Certificate.PairSemantics.raw6710step0 line 425
  90. def OAI.MUB6.Certificate.PairSemantics.raw6710step1 line 427
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical6710 line 429
  92. def OAI.MUB6.Certificate.PairSemantics.raw6711 line 442
  93. def OAI.MUB6.Certificate.PairSemantics.raw6711step0 line 444
  94. def OAI.MUB6.Certificate.PairSemantics.raw6711step1 line 446
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical6711 line 448
  96. def OAI.MUB6.Certificate.PairSemantics.raw6712 line 461
  97. def OAI.MUB6.Certificate.PairSemantics.raw6712step0 line 463
  98. def OAI.MUB6.Certificate.PairSemantics.raw6712step1 line 465
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical6712 line 467
  100. def OAI.MUB6.Certificate.PairSemantics.raw6713 line 480
  101. def OAI.MUB6.Certificate.PairSemantics.raw6713step0 line 482
  102. def OAI.MUB6.Certificate.PairSemantics.raw6713step1 line 484
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical6713 line 486
  104. def OAI.MUB6.Certificate.PairSemantics.raw6714 line 499
  105. def OAI.MUB6.Certificate.PairSemantics.raw6714step0 line 501
  106. def OAI.MUB6.Certificate.PairSemantics.raw6714step1 line 503
  107. def OAI.MUB6.Certificate.PairSemantics.raw6714step2 line 505
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical6714 line 507
  109. def OAI.MUB6.Certificate.PairSemantics.raw6715 line 524
  110. def OAI.MUB6.Certificate.PairSemantics.raw6715step0 line 526
  111. def OAI.MUB6.Certificate.PairSemantics.raw6715step1 line 528
  112. def OAI.MUB6.Certificate.PairSemantics.raw6715step2 line 530
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical6715 line 532
  114. def OAI.MUB6.Certificate.PairSemantics.raw6716 line 549
  115. def OAI.MUB6.Certificate.PairSemantics.raw6716step0 line 551
  116. def OAI.MUB6.Certificate.PairSemantics.raw6716step1 line 553
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical6716 line 555
  118. def OAI.MUB6.Certificate.PairSemantics.raw6717 line 568
  119. def OAI.MUB6.Certificate.PairSemantics.raw6717step0 line 570
  120. def OAI.MUB6.Certificate.PairSemantics.raw6717step1 line 572
  121. def OAI.MUB6.Certificate.PairSemantics.raw6717step2 line 574
  122. theorem OAI.MUB6.Certificate.PairSemantics.canonical6717 line 576
  123. def OAI.MUB6.Certificate.PairSemantics.raw6718 line 593
  124. def OAI.MUB6.Certificate.PairSemantics.raw6718step0 line 595
  125. def OAI.MUB6.Certificate.PairSemantics.raw6718step1 line 597
  126. theorem OAI.MUB6.Certificate.PairSemantics.canonical6718 line 599
  127. def OAI.MUB6.Certificate.PairSemantics.raw6719 line 612
  128. def OAI.MUB6.Certificate.PairSemantics.raw6719step0 line 614
  129. theorem OAI.MUB6.Certificate.PairSemantics.canonical6719 line 616