OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical250.lean

GitHub source file

123 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8000 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw8000step0 line 21
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical8000 line 23
  4. def OAI.MUB6.Certificate.PairSemantics.raw8001 line 32
  5. def OAI.MUB6.Certificate.PairSemantics.raw8001step0 line 34
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical8001 line 36
  7. def OAI.MUB6.Certificate.PairSemantics.raw8002 line 45
  8. def OAI.MUB6.Certificate.PairSemantics.raw8002step0 line 47
  9. def OAI.MUB6.Certificate.PairSemantics.raw8002step1 line 49
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical8002 line 51
  11. def OAI.MUB6.Certificate.PairSemantics.raw8003 line 66
  12. def OAI.MUB6.Certificate.PairSemantics.raw8003step0 line 68
  13. def OAI.MUB6.Certificate.PairSemantics.raw8003step1 line 70
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical8003 line 72
  15. def OAI.MUB6.Certificate.PairSemantics.raw8004 line 87
  16. def OAI.MUB6.Certificate.PairSemantics.raw8004step0 line 89
  17. def OAI.MUB6.Certificate.PairSemantics.raw8004step1 line 91
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical8004 line 93
  19. def OAI.MUB6.Certificate.PairSemantics.raw8005 line 107
  20. def OAI.MUB6.Certificate.PairSemantics.raw8005step0 line 109
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical8005 line 111
  22. def OAI.MUB6.Certificate.PairSemantics.raw8006 line 121
  23. def OAI.MUB6.Certificate.PairSemantics.raw8006step0 line 123
  24. def OAI.MUB6.Certificate.PairSemantics.raw8006step1 line 125
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical8006 line 127
  26. def OAI.MUB6.Certificate.PairSemantics.raw8007 line 142
  27. def OAI.MUB6.Certificate.PairSemantics.raw8007step0 line 144
  28. def OAI.MUB6.Certificate.PairSemantics.raw8007step1 line 146
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical8007 line 148
  30. def OAI.MUB6.Certificate.PairSemantics.raw8008 line 162
  31. def OAI.MUB6.Certificate.PairSemantics.raw8008step0 line 164
  32. def OAI.MUB6.Certificate.PairSemantics.raw8008step1 line 166
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical8008 line 168
  34. def OAI.MUB6.Certificate.PairSemantics.raw8009 line 181
  35. def OAI.MUB6.Certificate.PairSemantics.raw8009step0 line 183
  36. def OAI.MUB6.Certificate.PairSemantics.raw8009step1 line 185
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical8009 line 187
  38. def OAI.MUB6.Certificate.PairSemantics.raw8010 line 200
  39. def OAI.MUB6.Certificate.PairSemantics.raw8010step0 line 202
  40. def OAI.MUB6.Certificate.PairSemantics.raw8010step1 line 204
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical8010 line 206
  42. def OAI.MUB6.Certificate.PairSemantics.raw8011 line 219
  43. def OAI.MUB6.Certificate.PairSemantics.raw8011step0 line 221
  44. def OAI.MUB6.Certificate.PairSemantics.raw8011step1 line 223
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical8011 line 225
  46. def OAI.MUB6.Certificate.PairSemantics.raw8012 line 238
  47. def OAI.MUB6.Certificate.PairSemantics.raw8012step0 line 240
  48. def OAI.MUB6.Certificate.PairSemantics.raw8012step1 line 242
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical8012 line 244
  50. def OAI.MUB6.Certificate.PairSemantics.raw8013 line 257
  51. def OAI.MUB6.Certificate.PairSemantics.raw8013step0 line 259
  52. def OAI.MUB6.Certificate.PairSemantics.raw8013step1 line 261
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical8013 line 263
  54. def OAI.MUB6.Certificate.PairSemantics.raw8014 line 276
  55. def OAI.MUB6.Certificate.PairSemantics.raw8014step0 line 278
  56. def OAI.MUB6.Certificate.PairSemantics.raw8014step1 line 280
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical8014 line 282
  58. def OAI.MUB6.Certificate.PairSemantics.raw8015 line 295
  59. def OAI.MUB6.Certificate.PairSemantics.raw8015step0 line 297
  60. def OAI.MUB6.Certificate.PairSemantics.raw8015step1 line 299
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical8015 line 301
  62. def OAI.MUB6.Certificate.PairSemantics.raw8016 line 314
  63. def OAI.MUB6.Certificate.PairSemantics.raw8016step0 line 316
  64. def OAI.MUB6.Certificate.PairSemantics.raw8016step1 line 318
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical8016 line 320
  66. def OAI.MUB6.Certificate.PairSemantics.raw8017 line 333
  67. def OAI.MUB6.Certificate.PairSemantics.raw8017step0 line 335
  68. def OAI.MUB6.Certificate.PairSemantics.raw8017step1 line 337
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical8017 line 339
  70. def OAI.MUB6.Certificate.PairSemantics.raw8018 line 352
  71. def OAI.MUB6.Certificate.PairSemantics.raw8018step0 line 354
  72. def OAI.MUB6.Certificate.PairSemantics.raw8018step1 line 356
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical8018 line 358
  74. def OAI.MUB6.Certificate.PairSemantics.raw8019 line 373
  75. def OAI.MUB6.Certificate.PairSemantics.raw8019step0 line 375
  76. def OAI.MUB6.Certificate.PairSemantics.raw8019step1 line 377
  77. def OAI.MUB6.Certificate.PairSemantics.raw8019step2 line 379
  78. def OAI.MUB6.Certificate.PairSemantics.raw8019step3 line 381
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical8019 line 383
  80. def OAI.MUB6.Certificate.PairSemantics.raw8020 line 406
  81. def OAI.MUB6.Certificate.PairSemantics.raw8020step0 line 408
  82. def OAI.MUB6.Certificate.PairSemantics.raw8020step1 line 410
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical8020 line 412
  84. def OAI.MUB6.Certificate.PairSemantics.raw8021 line 425
  85. def OAI.MUB6.Certificate.PairSemantics.raw8021step0 line 427
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical8021 line 429
  87. def OAI.MUB6.Certificate.PairSemantics.raw8022 line 439
  88. def OAI.MUB6.Certificate.PairSemantics.raw8022step0 line 441
  89. def OAI.MUB6.Certificate.PairSemantics.raw8022step1 line 443
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical8022 line 445
  91. def OAI.MUB6.Certificate.PairSemantics.raw8023 line 460
  92. def OAI.MUB6.Certificate.PairSemantics.raw8023step0 line 462
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical8023 line 464
  94. def OAI.MUB6.Certificate.PairSemantics.raw8024 line 474
  95. def OAI.MUB6.Certificate.PairSemantics.raw8024step0 line 476
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical8024 line 478
  97. def OAI.MUB6.Certificate.PairSemantics.raw8025 line 488
  98. def OAI.MUB6.Certificate.PairSemantics.raw8025step0 line 490
  99. def OAI.MUB6.Certificate.PairSemantics.raw8025step1 line 492
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical8025 line 494
  101. def OAI.MUB6.Certificate.PairSemantics.raw8026 line 507
  102. def OAI.MUB6.Certificate.PairSemantics.raw8026step0 line 509
  103. def OAI.MUB6.Certificate.PairSemantics.raw8026step1 line 511
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical8026 line 513
  105. def OAI.MUB6.Certificate.PairSemantics.raw8027 line 526
  106. def OAI.MUB6.Certificate.PairSemantics.raw8027step0 line 528
  107. def OAI.MUB6.Certificate.PairSemantics.raw8027step1 line 530
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical8027 line 532
  109. def OAI.MUB6.Certificate.PairSemantics.raw8028 line 545
  110. def OAI.MUB6.Certificate.PairSemantics.raw8028step0 line 547
  111. def OAI.MUB6.Certificate.PairSemantics.raw8028step1 line 549
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical8028 line 551
  113. def OAI.MUB6.Certificate.PairSemantics.raw8029 line 564
  114. def OAI.MUB6.Certificate.PairSemantics.raw8029step0 line 566
  115. def OAI.MUB6.Certificate.PairSemantics.raw8029step1 line 568
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical8029 line 570
  117. def OAI.MUB6.Certificate.PairSemantics.raw8030 line 583
  118. def OAI.MUB6.Certificate.PairSemantics.raw8030step0 line 585
  119. def OAI.MUB6.Certificate.PairSemantics.raw8030step1 line 587
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical8030 line 589
  121. def OAI.MUB6.Certificate.PairSemantics.raw8031 line 602
  122. def OAI.MUB6.Certificate.PairSemantics.raw8031step0 line 604
  123. theorem OAI.MUB6.Certificate.PairSemantics.canonical8031 line 606