OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical113.lean

GitHub source file

126 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3616 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw3616step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw3616step1 line 23
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3616 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw3617 line 38
  6. def OAI.MUB6.Certificate.PairSemantics.raw3617step0 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw3617step1 line 42
  8. def OAI.MUB6.Certificate.PairSemantics.raw3617step2 line 44
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical3617 line 46
  10. def OAI.MUB6.Certificate.PairSemantics.raw3618 line 63
  11. def OAI.MUB6.Certificate.PairSemantics.raw3618step0 line 65
  12. def OAI.MUB6.Certificate.PairSemantics.raw3618step1 line 67
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical3618 line 69
  14. def OAI.MUB6.Certificate.PairSemantics.raw3619 line 82
  15. def OAI.MUB6.Certificate.PairSemantics.raw3619step0 line 84
  16. def OAI.MUB6.Certificate.PairSemantics.raw3619step1 line 86
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical3619 line 88
  18. def OAI.MUB6.Certificate.PairSemantics.raw3620 line 101
  19. def OAI.MUB6.Certificate.PairSemantics.raw3620step0 line 103
  20. def OAI.MUB6.Certificate.PairSemantics.raw3620step1 line 105
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical3620 line 107
  22. def OAI.MUB6.Certificate.PairSemantics.raw3621 line 120
  23. def OAI.MUB6.Certificate.PairSemantics.raw3621step0 line 122
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical3621 line 124
  25. def OAI.MUB6.Certificate.PairSemantics.raw3622 line 133
  26. def OAI.MUB6.Certificate.PairSemantics.raw3622step0 line 135
  27. def OAI.MUB6.Certificate.PairSemantics.raw3622step1 line 137
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical3622 line 139
  29. def OAI.MUB6.Certificate.PairSemantics.raw3623 line 152
  30. def OAI.MUB6.Certificate.PairSemantics.raw3623step0 line 154
  31. def OAI.MUB6.Certificate.PairSemantics.raw3623step1 line 156
  32. def OAI.MUB6.Certificate.PairSemantics.raw3623step2 line 158
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical3623 line 160
  34. def OAI.MUB6.Certificate.PairSemantics.raw3624 line 177
  35. def OAI.MUB6.Certificate.PairSemantics.raw3624step0 line 179
  36. def OAI.MUB6.Certificate.PairSemantics.raw3624step1 line 181
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical3624 line 183
  38. def OAI.MUB6.Certificate.PairSemantics.raw3625 line 196
  39. def OAI.MUB6.Certificate.PairSemantics.raw3625step0 line 198
  40. def OAI.MUB6.Certificate.PairSemantics.raw3625step1 line 200
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical3625 line 202
  42. def OAI.MUB6.Certificate.PairSemantics.raw3626 line 215
  43. def OAI.MUB6.Certificate.PairSemantics.raw3626step0 line 217
  44. def OAI.MUB6.Certificate.PairSemantics.raw3626step1 line 219
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical3626 line 221
  46. def OAI.MUB6.Certificate.PairSemantics.raw3627 line 234
  47. def OAI.MUB6.Certificate.PairSemantics.raw3627step0 line 236
  48. def OAI.MUB6.Certificate.PairSemantics.raw3627step1 line 238
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical3627 line 240
  50. def OAI.MUB6.Certificate.PairSemantics.raw3628 line 253
  51. def OAI.MUB6.Certificate.PairSemantics.raw3628step0 line 255
  52. def OAI.MUB6.Certificate.PairSemantics.raw3628step1 line 257
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical3628 line 259
  54. def OAI.MUB6.Certificate.PairSemantics.raw3629 line 272
  55. def OAI.MUB6.Certificate.PairSemantics.raw3629step0 line 274
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical3629 line 276
  57. def OAI.MUB6.Certificate.PairSemantics.raw3630 line 285
  58. def OAI.MUB6.Certificate.PairSemantics.raw3630step0 line 287
  59. def OAI.MUB6.Certificate.PairSemantics.raw3630step1 line 289
  60. def OAI.MUB6.Certificate.PairSemantics.raw3630step2 line 291
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical3630 line 293
  62. def OAI.MUB6.Certificate.PairSemantics.raw3631 line 310
  63. def OAI.MUB6.Certificate.PairSemantics.raw3631step0 line 312
  64. def OAI.MUB6.Certificate.PairSemantics.raw3631step1 line 314
  65. def OAI.MUB6.Certificate.PairSemantics.raw3631step2 line 316
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical3631 line 318
  67. def OAI.MUB6.Certificate.PairSemantics.raw3632 line 335
  68. def OAI.MUB6.Certificate.PairSemantics.raw3632step0 line 337
  69. def OAI.MUB6.Certificate.PairSemantics.raw3632step1 line 339
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical3632 line 341
  71. def OAI.MUB6.Certificate.PairSemantics.raw3633 line 354
  72. def OAI.MUB6.Certificate.PairSemantics.raw3633step0 line 356
  73. def OAI.MUB6.Certificate.PairSemantics.raw3633step1 line 358
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical3633 line 360
  75. def OAI.MUB6.Certificate.PairSemantics.raw3634 line 373
  76. def OAI.MUB6.Certificate.PairSemantics.raw3634step0 line 375
  77. def OAI.MUB6.Certificate.PairSemantics.raw3634step1 line 377
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical3634 line 379
  79. def OAI.MUB6.Certificate.PairSemantics.raw3635 line 392
  80. def OAI.MUB6.Certificate.PairSemantics.raw3635step0 line 394
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical3635 line 396
  82. def OAI.MUB6.Certificate.PairSemantics.raw3636 line 405
  83. def OAI.MUB6.Certificate.PairSemantics.raw3636step0 line 407
  84. def OAI.MUB6.Certificate.PairSemantics.raw3636step1 line 409
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical3636 line 411
  86. def OAI.MUB6.Certificate.PairSemantics.raw3637 line 424
  87. def OAI.MUB6.Certificate.PairSemantics.raw3637step0 line 426
  88. def OAI.MUB6.Certificate.PairSemantics.raw3637step1 line 428
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical3637 line 430
  90. def OAI.MUB6.Certificate.PairSemantics.raw3638 line 443
  91. def OAI.MUB6.Certificate.PairSemantics.raw3638step0 line 445
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical3638 line 447
  93. def OAI.MUB6.Certificate.PairSemantics.raw3639 line 456
  94. def OAI.MUB6.Certificate.PairSemantics.raw3639step0 line 458
  95. def OAI.MUB6.Certificate.PairSemantics.raw3639step1 line 460
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical3639 line 462
  97. def OAI.MUB6.Certificate.PairSemantics.raw3640 line 475
  98. def OAI.MUB6.Certificate.PairSemantics.raw3640step0 line 477
  99. def OAI.MUB6.Certificate.PairSemantics.raw3640step1 line 479
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical3640 line 481
  101. def OAI.MUB6.Certificate.PairSemantics.raw3641 line 494
  102. def OAI.MUB6.Certificate.PairSemantics.raw3641step0 line 496
  103. def OAI.MUB6.Certificate.PairSemantics.raw3641step1 line 498
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical3641 line 500
  105. def OAI.MUB6.Certificate.PairSemantics.raw3642 line 513
  106. def OAI.MUB6.Certificate.PairSemantics.raw3642step0 line 515
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical3642 line 517
  108. def OAI.MUB6.Certificate.PairSemantics.raw3643 line 526
  109. def OAI.MUB6.Certificate.PairSemantics.raw3643step0 line 528
  110. def OAI.MUB6.Certificate.PairSemantics.raw3643step1 line 530
  111. def OAI.MUB6.Certificate.PairSemantics.raw3643step2 line 532
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical3643 line 534
  113. def OAI.MUB6.Certificate.PairSemantics.raw3644 line 551
  114. def OAI.MUB6.Certificate.PairSemantics.raw3644step0 line 553
  115. def OAI.MUB6.Certificate.PairSemantics.raw3644step1 line 555
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical3644 line 557
  117. def OAI.MUB6.Certificate.PairSemantics.raw3645 line 570
  118. def OAI.MUB6.Certificate.PairSemantics.raw3645step0 line 572
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical3645 line 574
  120. def OAI.MUB6.Certificate.PairSemantics.raw3646 line 583
  121. def OAI.MUB6.Certificate.PairSemantics.raw3646step0 line 585
  122. def OAI.MUB6.Certificate.PairSemantics.raw3646step1 line 587
  123. theorem OAI.MUB6.Certificate.PairSemantics.canonical3646 line 589
  124. def OAI.MUB6.Certificate.PairSemantics.raw3647 line 602
  125. def OAI.MUB6.Certificate.PairSemantics.raw3647step0 line 604
  126. theorem OAI.MUB6.Certificate.PairSemantics.canonical3647 line 606