OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical242.lean

GitHub source file

121 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7744 line 16
  2. def OAI.MUB6.Certificate.PairSemantics.raw7744step0 line 18
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical7744 line 20
  4. def OAI.MUB6.Certificate.PairSemantics.raw7745 line 29
  5. def OAI.MUB6.Certificate.PairSemantics.raw7745step0 line 31
  6. def OAI.MUB6.Certificate.PairSemantics.raw7745step1 line 33
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical7745 line 35
  8. def OAI.MUB6.Certificate.PairSemantics.raw7746 line 49
  9. def OAI.MUB6.Certificate.PairSemantics.raw7746step0 line 51
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical7746 line 53
  11. def OAI.MUB6.Certificate.PairSemantics.raw7747 line 62
  12. def OAI.MUB6.Certificate.PairSemantics.raw7747step0 line 64
  13. def OAI.MUB6.Certificate.PairSemantics.raw7747step1 line 66
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical7747 line 68
  15. def OAI.MUB6.Certificate.PairSemantics.raw7748 line 82
  16. def OAI.MUB6.Certificate.PairSemantics.raw7748step0 line 84
  17. def OAI.MUB6.Certificate.PairSemantics.raw7748step1 line 86
  18. def OAI.MUB6.Certificate.PairSemantics.raw7748step2 line 88
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical7748 line 90
  20. def OAI.MUB6.Certificate.PairSemantics.raw7749 line 109
  21. def OAI.MUB6.Certificate.PairSemantics.raw7749step0 line 111
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical7749 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw7750 line 122
  24. def OAI.MUB6.Certificate.PairSemantics.raw7750step0 line 124
  25. def OAI.MUB6.Certificate.PairSemantics.raw7750step1 line 126
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical7750 line 128
  27. def OAI.MUB6.Certificate.PairSemantics.raw7751 line 142
  28. def OAI.MUB6.Certificate.PairSemantics.raw7751step0 line 144
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical7751 line 146
  30. def OAI.MUB6.Certificate.PairSemantics.raw7752 line 155
  31. def OAI.MUB6.Certificate.PairSemantics.raw7752step0 line 157
  32. def OAI.MUB6.Certificate.PairSemantics.raw7752step1 line 159
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical7752 line 161
  34. def OAI.MUB6.Certificate.PairSemantics.raw7753 line 175
  35. def OAI.MUB6.Certificate.PairSemantics.raw7753step0 line 177
  36. def OAI.MUB6.Certificate.PairSemantics.raw7753step1 line 179
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical7753 line 181
  38. def OAI.MUB6.Certificate.PairSemantics.raw7754 line 195
  39. def OAI.MUB6.Certificate.PairSemantics.raw7754step0 line 197
  40. def OAI.MUB6.Certificate.PairSemantics.raw7754step1 line 199
  41. def OAI.MUB6.Certificate.PairSemantics.raw7754step2 line 201
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical7754 line 203
  43. def OAI.MUB6.Certificate.PairSemantics.raw7755 line 222
  44. def OAI.MUB6.Certificate.PairSemantics.raw7755step0 line 224
  45. def OAI.MUB6.Certificate.PairSemantics.raw7755step1 line 226
  46. def OAI.MUB6.Certificate.PairSemantics.raw7755step2 line 228
  47. def OAI.MUB6.Certificate.PairSemantics.raw7755step3 line 230
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical7755 line 232
  49. def OAI.MUB6.Certificate.PairSemantics.raw7756 line 256
  50. def OAI.MUB6.Certificate.PairSemantics.raw7756step0 line 258
  51. def OAI.MUB6.Certificate.PairSemantics.raw7756step1 line 260
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical7756 line 262
  53. def OAI.MUB6.Certificate.PairSemantics.raw7757 line 276
  54. def OAI.MUB6.Certificate.PairSemantics.raw7757step0 line 278
  55. def OAI.MUB6.Certificate.PairSemantics.raw7757step1 line 280
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical7757 line 282
  57. def OAI.MUB6.Certificate.PairSemantics.raw7758 line 296
  58. def OAI.MUB6.Certificate.PairSemantics.raw7758step0 line 298
  59. def OAI.MUB6.Certificate.PairSemantics.raw7758step1 line 300
  60. def OAI.MUB6.Certificate.PairSemantics.raw7758step2 line 302
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical7758 line 304
  62. def OAI.MUB6.Certificate.PairSemantics.raw7759 line 323
  63. def OAI.MUB6.Certificate.PairSemantics.raw7759step0 line 325
  64. def OAI.MUB6.Certificate.PairSemantics.raw7759step1 line 327
  65. def OAI.MUB6.Certificate.PairSemantics.raw7759step2 line 329
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical7759 line 331
  67. def OAI.MUB6.Certificate.PairSemantics.raw7760 line 350
  68. def OAI.MUB6.Certificate.PairSemantics.raw7760step0 line 352
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical7760 line 354
  70. def OAI.MUB6.Certificate.PairSemantics.raw7761 line 363
  71. def OAI.MUB6.Certificate.PairSemantics.raw7761step0 line 365
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical7761 line 367
  73. def OAI.MUB6.Certificate.PairSemantics.raw7762 line 376
  74. def OAI.MUB6.Certificate.PairSemantics.raw7762step0 line 378
  75. def OAI.MUB6.Certificate.PairSemantics.raw7762step1 line 380
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical7762 line 382
  77. def OAI.MUB6.Certificate.PairSemantics.raw7763 line 395
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical7763 line 397
  79. def OAI.MUB6.Certificate.PairSemantics.raw7764 line 401
  80. def OAI.MUB6.Certificate.PairSemantics.raw7764step0 line 403
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical7764 line 405
  82. def OAI.MUB6.Certificate.PairSemantics.raw7765 line 414
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical7765 line 416
  84. def OAI.MUB6.Certificate.PairSemantics.raw7766 line 420
  85. def OAI.MUB6.Certificate.PairSemantics.raw7766step0 line 422
  86. def OAI.MUB6.Certificate.PairSemantics.raw7766step1 line 424
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical7766 line 426
  88. def OAI.MUB6.Certificate.PairSemantics.raw7767 line 439
  89. def OAI.MUB6.Certificate.PairSemantics.raw7767step0 line 441
  90. def OAI.MUB6.Certificate.PairSemantics.raw7767step1 line 443
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical7767 line 445
  92. def OAI.MUB6.Certificate.PairSemantics.raw7768 line 458
  93. def OAI.MUB6.Certificate.PairSemantics.raw7768step0 line 460
  94. def OAI.MUB6.Certificate.PairSemantics.raw7768step1 line 462
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical7768 line 464
  96. def OAI.MUB6.Certificate.PairSemantics.raw7769 line 477
  97. def OAI.MUB6.Certificate.PairSemantics.raw7769step0 line 479
  98. def OAI.MUB6.Certificate.PairSemantics.raw7769step1 line 481
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical7769 line 483
  100. def OAI.MUB6.Certificate.PairSemantics.raw7770 line 496
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical7770 line 498
  102. def OAI.MUB6.Certificate.PairSemantics.raw7771 line 502
  103. def OAI.MUB6.Certificate.PairSemantics.raw7771step0 line 504
  104. def OAI.MUB6.Certificate.PairSemantics.raw7771step1 line 506
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical7771 line 508
  106. def OAI.MUB6.Certificate.PairSemantics.raw7772 line 521
  107. def OAI.MUB6.Certificate.PairSemantics.raw7772step0 line 523
  108. def OAI.MUB6.Certificate.PairSemantics.raw7772step1 line 525
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical7772 line 527
  110. def OAI.MUB6.Certificate.PairSemantics.raw7773 line 540
  111. def OAI.MUB6.Certificate.PairSemantics.raw7773step0 line 542
  112. def OAI.MUB6.Certificate.PairSemantics.raw7773step1 line 544
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical7773 line 546
  114. def OAI.MUB6.Certificate.PairSemantics.raw7774 line 559
  115. def OAI.MUB6.Certificate.PairSemantics.raw7774step0 line 561
  116. def OAI.MUB6.Certificate.PairSemantics.raw7774step1 line 563
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical7774 line 565
  118. def OAI.MUB6.Certificate.PairSemantics.raw7775 line 578
  119. def OAI.MUB6.Certificate.PairSemantics.raw7775step0 line 580
  120. def OAI.MUB6.Certificate.PairSemantics.raw7775step1 line 582
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical7775 line 584