OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical233.lean

GitHub source file

129 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7456 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw7456step0 line 17
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical7456 line 19
  4. def OAI.MUB6.Certificate.PairSemantics.raw7457 line 28
  5. def OAI.MUB6.Certificate.PairSemantics.raw7457step0 line 30
  6. def OAI.MUB6.Certificate.PairSemantics.raw7457step1 line 32
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical7457 line 34
  8. def OAI.MUB6.Certificate.PairSemantics.raw7458 line 47
  9. def OAI.MUB6.Certificate.PairSemantics.raw7458step0 line 49
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical7458 line 51
  11. def OAI.MUB6.Certificate.PairSemantics.raw7459 line 60
  12. def OAI.MUB6.Certificate.PairSemantics.raw7459step0 line 62
  13. def OAI.MUB6.Certificate.PairSemantics.raw7459step1 line 64
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical7459 line 66
  15. def OAI.MUB6.Certificate.PairSemantics.raw7460 line 79
  16. def OAI.MUB6.Certificate.PairSemantics.raw7460step0 line 81
  17. def OAI.MUB6.Certificate.PairSemantics.raw7460step1 line 83
  18. def OAI.MUB6.Certificate.PairSemantics.raw7460step2 line 85
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical7460 line 87
  20. def OAI.MUB6.Certificate.PairSemantics.raw7461 line 105
  21. def OAI.MUB6.Certificate.PairSemantics.raw7461step0 line 107
  22. def OAI.MUB6.Certificate.PairSemantics.raw7461step1 line 109
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical7461 line 111
  24. def OAI.MUB6.Certificate.PairSemantics.raw7462 line 124
  25. def OAI.MUB6.Certificate.PairSemantics.raw7462step0 line 126
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical7462 line 128
  27. def OAI.MUB6.Certificate.PairSemantics.raw7463 line 138
  28. def OAI.MUB6.Certificate.PairSemantics.raw7463step0 line 140
  29. def OAI.MUB6.Certificate.PairSemantics.raw7463step1 line 142
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical7463 line 144
  31. def OAI.MUB6.Certificate.PairSemantics.raw7464 line 157
  32. def OAI.MUB6.Certificate.PairSemantics.raw7464step0 line 159
  33. def OAI.MUB6.Certificate.PairSemantics.raw7464step1 line 161
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical7464 line 163
  35. def OAI.MUB6.Certificate.PairSemantics.raw7465 line 176
  36. def OAI.MUB6.Certificate.PairSemantics.raw7465step0 line 178
  37. def OAI.MUB6.Certificate.PairSemantics.raw7465step1 line 180
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical7465 line 182
  39. def OAI.MUB6.Certificate.PairSemantics.raw7466 line 195
  40. def OAI.MUB6.Certificate.PairSemantics.raw7466step0 line 197
  41. def OAI.MUB6.Certificate.PairSemantics.raw7466step1 line 199
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical7466 line 201
  43. def OAI.MUB6.Certificate.PairSemantics.raw7467 line 214
  44. def OAI.MUB6.Certificate.PairSemantics.raw7467step0 line 216
  45. def OAI.MUB6.Certificate.PairSemantics.raw7467step1 line 218
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical7467 line 220
  47. def OAI.MUB6.Certificate.PairSemantics.raw7468 line 233
  48. def OAI.MUB6.Certificate.PairSemantics.raw7468step0 line 235
  49. def OAI.MUB6.Certificate.PairSemantics.raw7468step1 line 237
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical7468 line 239
  51. def OAI.MUB6.Certificate.PairSemantics.raw7469 line 252
  52. def OAI.MUB6.Certificate.PairSemantics.raw7469step0 line 254
  53. def OAI.MUB6.Certificate.PairSemantics.raw7469step1 line 256
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical7469 line 258
  55. def OAI.MUB6.Certificate.PairSemantics.raw7470 line 271
  56. def OAI.MUB6.Certificate.PairSemantics.raw7470step0 line 273
  57. def OAI.MUB6.Certificate.PairSemantics.raw7470step1 line 275
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical7470 line 277
  59. def OAI.MUB6.Certificate.PairSemantics.raw7471 line 290
  60. def OAI.MUB6.Certificate.PairSemantics.raw7471step0 line 292
  61. def OAI.MUB6.Certificate.PairSemantics.raw7471step1 line 294
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical7471 line 296
  63. def OAI.MUB6.Certificate.PairSemantics.raw7472 line 309
  64. def OAI.MUB6.Certificate.PairSemantics.raw7472step0 line 311
  65. def OAI.MUB6.Certificate.PairSemantics.raw7472step1 line 313
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical7472 line 315
  67. def OAI.MUB6.Certificate.PairSemantics.raw7473 line 328
  68. def OAI.MUB6.Certificate.PairSemantics.raw7473step0 line 330
  69. def OAI.MUB6.Certificate.PairSemantics.raw7473step1 line 332
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical7473 line 334
  71. def OAI.MUB6.Certificate.PairSemantics.raw7474 line 347
  72. def OAI.MUB6.Certificate.PairSemantics.raw7474step0 line 349
  73. def OAI.MUB6.Certificate.PairSemantics.raw7474step1 line 351
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical7474 line 353
  75. def OAI.MUB6.Certificate.PairSemantics.raw7475 line 366
  76. def OAI.MUB6.Certificate.PairSemantics.raw7475step0 line 368
  77. def OAI.MUB6.Certificate.PairSemantics.raw7475step1 line 370
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical7475 line 372
  79. def OAI.MUB6.Certificate.PairSemantics.raw7476 line 385
  80. def OAI.MUB6.Certificate.PairSemantics.raw7476step0 line 387
  81. def OAI.MUB6.Certificate.PairSemantics.raw7476step1 line 389
  82. def OAI.MUB6.Certificate.PairSemantics.raw7476step2 line 391
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical7476 line 393
  84. def OAI.MUB6.Certificate.PairSemantics.raw7477 line 410
  85. def OAI.MUB6.Certificate.PairSemantics.raw7477step0 line 412
  86. def OAI.MUB6.Certificate.PairSemantics.raw7477step1 line 414
  87. def OAI.MUB6.Certificate.PairSemantics.raw7477step2 line 416
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical7477 line 418
  89. def OAI.MUB6.Certificate.PairSemantics.raw7478 line 435
  90. def OAI.MUB6.Certificate.PairSemantics.raw7478step0 line 437
  91. def OAI.MUB6.Certificate.PairSemantics.raw7478step1 line 439
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical7478 line 441
  93. def OAI.MUB6.Certificate.PairSemantics.raw7479 line 454
  94. def OAI.MUB6.Certificate.PairSemantics.raw7479step0 line 456
  95. def OAI.MUB6.Certificate.PairSemantics.raw7479step1 line 458
  96. def OAI.MUB6.Certificate.PairSemantics.raw7479step2 line 460
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical7479 line 462
  98. def OAI.MUB6.Certificate.PairSemantics.raw7480 line 479
  99. def OAI.MUB6.Certificate.PairSemantics.raw7480step0 line 481
  100. def OAI.MUB6.Certificate.PairSemantics.raw7480step1 line 483
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical7480 line 485
  102. def OAI.MUB6.Certificate.PairSemantics.raw7481 line 498
  103. def OAI.MUB6.Certificate.PairSemantics.raw7481step0 line 500
  104. def OAI.MUB6.Certificate.PairSemantics.raw7481step1 line 502
  105. def OAI.MUB6.Certificate.PairSemantics.raw7481step2 line 504
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical7481 line 506
  107. def OAI.MUB6.Certificate.PairSemantics.raw7482 line 523
  108. def OAI.MUB6.Certificate.PairSemantics.raw7482step0 line 525
  109. def OAI.MUB6.Certificate.PairSemantics.raw7482step1 line 527
  110. def OAI.MUB6.Certificate.PairSemantics.raw7482step2 line 529
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical7482 line 531
  112. def OAI.MUB6.Certificate.PairSemantics.raw7483 line 548
  113. def OAI.MUB6.Certificate.PairSemantics.raw7483step0 line 550
  114. def OAI.MUB6.Certificate.PairSemantics.raw7483step1 line 552
  115. def OAI.MUB6.Certificate.PairSemantics.raw7483step2 line 554
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical7483 line 556
  117. def OAI.MUB6.Certificate.PairSemantics.raw7484 line 573
  118. def OAI.MUB6.Certificate.PairSemantics.raw7484step0 line 575
  119. def OAI.MUB6.Certificate.PairSemantics.raw7484step1 line 577
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical7484 line 579
  121. def OAI.MUB6.Certificate.PairSemantics.raw7485 line 592
  122. def OAI.MUB6.Certificate.PairSemantics.raw7485step0 line 594
  123. theorem OAI.MUB6.Certificate.PairSemantics.canonical7485 line 596
  124. def OAI.MUB6.Certificate.PairSemantics.raw7486 line 605
  125. def OAI.MUB6.Certificate.PairSemantics.raw7486step0 line 607
  126. theorem OAI.MUB6.Certificate.PairSemantics.canonical7486 line 609
  127. def OAI.MUB6.Certificate.PairSemantics.raw7487 line 618
  128. def OAI.MUB6.Certificate.PairSemantics.raw7487step0 line 620
  129. theorem OAI.MUB6.Certificate.PairSemantics.canonical7487 line 622