OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical94.lean

GitHub source file

123 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3008 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw3008step0 line 20
  3. def OAI.MUB6.Certificate.PairSemantics.raw3008step1 line 22
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3008 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw3009 line 37
  6. def OAI.MUB6.Certificate.PairSemantics.raw3009step0 line 39
  7. def OAI.MUB6.Certificate.PairSemantics.raw3009step1 line 41
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical3009 line 43
  9. def OAI.MUB6.Certificate.PairSemantics.raw3010 line 56
  10. def OAI.MUB6.Certificate.PairSemantics.raw3010step0 line 58
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical3010 line 60
  12. def OAI.MUB6.Certificate.PairSemantics.raw3011 line 69
  13. def OAI.MUB6.Certificate.PairSemantics.raw3011step0 line 71
  14. def OAI.MUB6.Certificate.PairSemantics.raw3011step1 line 73
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical3011 line 75
  16. def OAI.MUB6.Certificate.PairSemantics.raw3012 line 88
  17. def OAI.MUB6.Certificate.PairSemantics.raw3012step0 line 90
  18. def OAI.MUB6.Certificate.PairSemantics.raw3012step1 line 92
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical3012 line 94
  20. def OAI.MUB6.Certificate.PairSemantics.raw3013 line 107
  21. def OAI.MUB6.Certificate.PairSemantics.raw3013step0 line 109
  22. def OAI.MUB6.Certificate.PairSemantics.raw3013step1 line 111
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical3013 line 113
  24. def OAI.MUB6.Certificate.PairSemantics.raw3014 line 126
  25. def OAI.MUB6.Certificate.PairSemantics.raw3014step0 line 128
  26. def OAI.MUB6.Certificate.PairSemantics.raw3014step1 line 130
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical3014 line 132
  28. def OAI.MUB6.Certificate.PairSemantics.raw3015 line 145
  29. def OAI.MUB6.Certificate.PairSemantics.raw3015step0 line 147
  30. def OAI.MUB6.Certificate.PairSemantics.raw3015step1 line 149
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical3015 line 151
  32. def OAI.MUB6.Certificate.PairSemantics.raw3016 line 164
  33. def OAI.MUB6.Certificate.PairSemantics.raw3016step0 line 166
  34. def OAI.MUB6.Certificate.PairSemantics.raw3016step1 line 168
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical3016 line 170
  36. def OAI.MUB6.Certificate.PairSemantics.raw3017 line 183
  37. def OAI.MUB6.Certificate.PairSemantics.raw3017step0 line 185
  38. def OAI.MUB6.Certificate.PairSemantics.raw3017step1 line 187
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical3017 line 189
  40. def OAI.MUB6.Certificate.PairSemantics.raw3018 line 202
  41. def OAI.MUB6.Certificate.PairSemantics.raw3018step0 line 204
  42. def OAI.MUB6.Certificate.PairSemantics.raw3018step1 line 206
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical3018 line 208
  44. def OAI.MUB6.Certificate.PairSemantics.raw3019 line 221
  45. def OAI.MUB6.Certificate.PairSemantics.raw3019step0 line 223
  46. def OAI.MUB6.Certificate.PairSemantics.raw3019step1 line 225
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical3019 line 227
  48. def OAI.MUB6.Certificate.PairSemantics.raw3020 line 240
  49. def OAI.MUB6.Certificate.PairSemantics.raw3020step0 line 242
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical3020 line 244
  51. def OAI.MUB6.Certificate.PairSemantics.raw3021 line 253
  52. def OAI.MUB6.Certificate.PairSemantics.raw3021step0 line 255
  53. def OAI.MUB6.Certificate.PairSemantics.raw3021step1 line 257
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical3021 line 259
  55. def OAI.MUB6.Certificate.PairSemantics.raw3022 line 272
  56. def OAI.MUB6.Certificate.PairSemantics.raw3022step0 line 274
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical3022 line 276
  58. def OAI.MUB6.Certificate.PairSemantics.raw3023 line 285
  59. def OAI.MUB6.Certificate.PairSemantics.raw3023step0 line 287
  60. def OAI.MUB6.Certificate.PairSemantics.raw3023step1 line 289
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical3023 line 291
  62. def OAI.MUB6.Certificate.PairSemantics.raw3024 line 304
  63. def OAI.MUB6.Certificate.PairSemantics.raw3024step0 line 306
  64. def OAI.MUB6.Certificate.PairSemantics.raw3024step1 line 308
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical3024 line 310
  66. def OAI.MUB6.Certificate.PairSemantics.raw3025 line 323
  67. def OAI.MUB6.Certificate.PairSemantics.raw3025step0 line 325
  68. def OAI.MUB6.Certificate.PairSemantics.raw3025step1 line 327
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical3025 line 329
  70. def OAI.MUB6.Certificate.PairSemantics.raw3026 line 342
  71. def OAI.MUB6.Certificate.PairSemantics.raw3026step0 line 344
  72. def OAI.MUB6.Certificate.PairSemantics.raw3026step1 line 346
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical3026 line 348
  74. def OAI.MUB6.Certificate.PairSemantics.raw3027 line 361
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical3027 line 363
  76. def OAI.MUB6.Certificate.PairSemantics.raw3028 line 367
  77. def OAI.MUB6.Certificate.PairSemantics.raw3028step0 line 369
  78. def OAI.MUB6.Certificate.PairSemantics.raw3028step1 line 371
  79. def OAI.MUB6.Certificate.PairSemantics.raw3028step2 line 373
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical3028 line 375
  81. def OAI.MUB6.Certificate.PairSemantics.raw3029 line 392
  82. def OAI.MUB6.Certificate.PairSemantics.raw3029step0 line 394
  83. def OAI.MUB6.Certificate.PairSemantics.raw3029step1 line 396
  84. def OAI.MUB6.Certificate.PairSemantics.raw3029step2 line 398
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical3029 line 400
  86. def OAI.MUB6.Certificate.PairSemantics.raw3030 line 417
  87. def OAI.MUB6.Certificate.PairSemantics.raw3030step0 line 419
  88. def OAI.MUB6.Certificate.PairSemantics.raw3030step1 line 421
  89. def OAI.MUB6.Certificate.PairSemantics.raw3030step2 line 423
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical3030 line 425
  91. def OAI.MUB6.Certificate.PairSemantics.raw3031 line 442
  92. def OAI.MUB6.Certificate.PairSemantics.raw3031step0 line 444
  93. def OAI.MUB6.Certificate.PairSemantics.raw3031step1 line 446
  94. def OAI.MUB6.Certificate.PairSemantics.raw3031step2 line 448
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical3031 line 450
  96. def OAI.MUB6.Certificate.PairSemantics.raw3032 line 467
  97. def OAI.MUB6.Certificate.PairSemantics.raw3032step0 line 469
  98. def OAI.MUB6.Certificate.PairSemantics.raw3032step1 line 471
  99. def OAI.MUB6.Certificate.PairSemantics.raw3032step2 line 473
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical3032 line 475
  101. def OAI.MUB6.Certificate.PairSemantics.raw3033 line 492
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical3033 line 494
  103. def OAI.MUB6.Certificate.PairSemantics.raw3034 line 498
  104. def OAI.MUB6.Certificate.PairSemantics.raw3034step0 line 500
  105. def OAI.MUB6.Certificate.PairSemantics.raw3034step1 line 502
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical3034 line 504
  107. def OAI.MUB6.Certificate.PairSemantics.raw3035 line 517
  108. def OAI.MUB6.Certificate.PairSemantics.raw3035step0 line 519
  109. def OAI.MUB6.Certificate.PairSemantics.raw3035step1 line 521
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical3035 line 523
  111. def OAI.MUB6.Certificate.PairSemantics.raw3036 line 536
  112. def OAI.MUB6.Certificate.PairSemantics.raw3036step0 line 538
  113. def OAI.MUB6.Certificate.PairSemantics.raw3036step1 line 540
  114. def OAI.MUB6.Certificate.PairSemantics.raw3036step2 line 542
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical3036 line 544
  116. def OAI.MUB6.Certificate.PairSemantics.raw3037 line 561
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical3037 line 563
  118. def OAI.MUB6.Certificate.PairSemantics.raw3038 line 567
  119. def OAI.MUB6.Certificate.PairSemantics.raw3038step0 line 569
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical3038 line 571
  121. def OAI.MUB6.Certificate.PairSemantics.raw3039 line 580
  122. def OAI.MUB6.Certificate.PairSemantics.raw3039step0 line 582
  123. theorem OAI.MUB6.Certificate.PairSemantics.canonical3039 line 584