OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical105.lean

GitHub source file

124 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3360 line 27
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical3360 line 29
  3. def OAI.MUB6.Certificate.PairSemantics.raw3361 line 33
  4. def OAI.MUB6.Certificate.PairSemantics.raw3361step0 line 35
  5. def OAI.MUB6.Certificate.PairSemantics.raw3361step1 line 37
  6. def OAI.MUB6.Certificate.PairSemantics.raw3361step2 line 39
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical3361 line 41
  8. def OAI.MUB6.Certificate.PairSemantics.raw3362 line 58
  9. def OAI.MUB6.Certificate.PairSemantics.raw3362step0 line 60
  10. def OAI.MUB6.Certificate.PairSemantics.raw3362step1 line 62
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical3362 line 64
  12. def OAI.MUB6.Certificate.PairSemantics.raw3363 line 77
  13. def OAI.MUB6.Certificate.PairSemantics.raw3363step0 line 79
  14. def OAI.MUB6.Certificate.PairSemantics.raw3363step1 line 81
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical3363 line 83
  16. def OAI.MUB6.Certificate.PairSemantics.raw3364 line 96
  17. def OAI.MUB6.Certificate.PairSemantics.raw3364step0 line 98
  18. def OAI.MUB6.Certificate.PairSemantics.raw3364step1 line 100
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical3364 line 102
  20. def OAI.MUB6.Certificate.PairSemantics.raw3365 line 115
  21. def OAI.MUB6.Certificate.PairSemantics.raw3365step0 line 117
  22. def OAI.MUB6.Certificate.PairSemantics.raw3365step1 line 119
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical3365 line 121
  24. def OAI.MUB6.Certificate.PairSemantics.raw3366 line 134
  25. def OAI.MUB6.Certificate.PairSemantics.raw3366step0 line 136
  26. def OAI.MUB6.Certificate.PairSemantics.raw3366step1 line 138
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical3366 line 140
  28. def OAI.MUB6.Certificate.PairSemantics.raw3367 line 153
  29. def OAI.MUB6.Certificate.PairSemantics.raw3367step0 line 155
  30. def OAI.MUB6.Certificate.PairSemantics.raw3367step1 line 157
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical3367 line 159
  32. def OAI.MUB6.Certificate.PairSemantics.raw3368 line 172
  33. def OAI.MUB6.Certificate.PairSemantics.raw3368step0 line 174
  34. def OAI.MUB6.Certificate.PairSemantics.raw3368step1 line 176
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical3368 line 178
  36. def OAI.MUB6.Certificate.PairSemantics.raw3369 line 191
  37. def OAI.MUB6.Certificate.PairSemantics.raw3369step0 line 193
  38. def OAI.MUB6.Certificate.PairSemantics.raw3369step1 line 195
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical3369 line 197
  40. def OAI.MUB6.Certificate.PairSemantics.raw3370 line 210
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical3370 line 212
  42. def OAI.MUB6.Certificate.PairSemantics.raw3371 line 216
  43. def OAI.MUB6.Certificate.PairSemantics.raw3371step0 line 218
  44. def OAI.MUB6.Certificate.PairSemantics.raw3371step1 line 220
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical3371 line 222
  46. def OAI.MUB6.Certificate.PairSemantics.raw3372 line 235
  47. def OAI.MUB6.Certificate.PairSemantics.raw3372step0 line 237
  48. def OAI.MUB6.Certificate.PairSemantics.raw3372step1 line 239
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical3372 line 241
  50. def OAI.MUB6.Certificate.PairSemantics.raw3373 line 254
  51. def OAI.MUB6.Certificate.PairSemantics.raw3373step0 line 256
  52. def OAI.MUB6.Certificate.PairSemantics.raw3373step1 line 258
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical3373 line 260
  54. def OAI.MUB6.Certificate.PairSemantics.raw3374 line 273
  55. def OAI.MUB6.Certificate.PairSemantics.raw3374step0 line 275
  56. def OAI.MUB6.Certificate.PairSemantics.raw3374step1 line 277
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical3374 line 279
  58. def OAI.MUB6.Certificate.PairSemantics.raw3375 line 292
  59. def OAI.MUB6.Certificate.PairSemantics.raw3375step0 line 294
  60. def OAI.MUB6.Certificate.PairSemantics.raw3375step1 line 296
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical3375 line 298
  62. def OAI.MUB6.Certificate.PairSemantics.raw3376 line 311
  63. def OAI.MUB6.Certificate.PairSemantics.raw3376step0 line 313
  64. def OAI.MUB6.Certificate.PairSemantics.raw3376step1 line 315
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical3376 line 317
  66. def OAI.MUB6.Certificate.PairSemantics.raw3377 line 330
  67. def OAI.MUB6.Certificate.PairSemantics.raw3377step0 line 332
  68. def OAI.MUB6.Certificate.PairSemantics.raw3377step1 line 334
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical3377 line 336
  70. def OAI.MUB6.Certificate.PairSemantics.raw3378 line 349
  71. def OAI.MUB6.Certificate.PairSemantics.raw3378step0 line 351
  72. def OAI.MUB6.Certificate.PairSemantics.raw3378step1 line 353
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical3378 line 355
  74. def OAI.MUB6.Certificate.PairSemantics.raw3379 line 368
  75. def OAI.MUB6.Certificate.PairSemantics.raw3379step0 line 370
  76. def OAI.MUB6.Certificate.PairSemantics.raw3379step1 line 372
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical3379 line 374
  78. def OAI.MUB6.Certificate.PairSemantics.raw3380 line 387
  79. def OAI.MUB6.Certificate.PairSemantics.raw3380step0 line 389
  80. def OAI.MUB6.Certificate.PairSemantics.raw3380step1 line 391
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical3380 line 393
  82. def OAI.MUB6.Certificate.PairSemantics.raw3381 line 406
  83. def OAI.MUB6.Certificate.PairSemantics.raw3381step0 line 408
  84. def OAI.MUB6.Certificate.PairSemantics.raw3381step1 line 410
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical3381 line 412
  86. def OAI.MUB6.Certificate.PairSemantics.raw3382 line 425
  87. def OAI.MUB6.Certificate.PairSemantics.raw3382step0 line 427
  88. def OAI.MUB6.Certificate.PairSemantics.raw3382step1 line 429
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical3382 line 431
  90. def OAI.MUB6.Certificate.PairSemantics.raw3383 line 445
  91. def OAI.MUB6.Certificate.PairSemantics.raw3383step0 line 447
  92. def OAI.MUB6.Certificate.PairSemantics.raw3383step1 line 449
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical3383 line 451
  94. def OAI.MUB6.Certificate.PairSemantics.raw3384 line 465
  95. def OAI.MUB6.Certificate.PairSemantics.raw3384step0 line 467
  96. def OAI.MUB6.Certificate.PairSemantics.raw3384step1 line 469
  97. def OAI.MUB6.Certificate.PairSemantics.raw3384step2 line 471
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical3384 line 473
  99. def OAI.MUB6.Certificate.PairSemantics.raw3385 line 491
  100. def OAI.MUB6.Certificate.PairSemantics.raw3385step0 line 493
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical3385 line 495
  102. def OAI.MUB6.Certificate.PairSemantics.raw3386 line 504
  103. def OAI.MUB6.Certificate.PairSemantics.raw3386step0 line 506
  104. def OAI.MUB6.Certificate.PairSemantics.raw3386step1 line 508
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical3386 line 510
  106. def OAI.MUB6.Certificate.PairSemantics.raw3387 line 523
  107. def OAI.MUB6.Certificate.PairSemantics.raw3387step0 line 525
  108. def OAI.MUB6.Certificate.PairSemantics.raw3387step1 line 527
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical3387 line 529
  110. def OAI.MUB6.Certificate.PairSemantics.raw3388 line 542
  111. def OAI.MUB6.Certificate.PairSemantics.raw3388step0 line 544
  112. def OAI.MUB6.Certificate.PairSemantics.raw3388step1 line 546
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical3388 line 548
  114. def OAI.MUB6.Certificate.PairSemantics.raw3389 line 562
  115. def OAI.MUB6.Certificate.PairSemantics.raw3389step0 line 564
  116. def OAI.MUB6.Certificate.PairSemantics.raw3389step1 line 566
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical3389 line 568
  118. def OAI.MUB6.Certificate.PairSemantics.raw3390 line 581
  119. def OAI.MUB6.Certificate.PairSemantics.raw3390step0 line 583
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical3390 line 585
  121. def OAI.MUB6.Certificate.PairSemantics.raw3391 line 594
  122. def OAI.MUB6.Certificate.PairSemantics.raw3391step0 line 596
  123. def OAI.MUB6.Certificate.PairSemantics.raw3391step1 line 598
  124. theorem OAI.MUB6.Certificate.PairSemantics.canonical3391 line 600