OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical4.lean

GitHub source file

121 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw128 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw128step0 line 17
  3. def OAI.MUB6.Certificate.PairSemantics.raw128step1 line 19
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical128 line 21
  5. def OAI.MUB6.Certificate.PairSemantics.raw129 line 34
  6. def OAI.MUB6.Certificate.PairSemantics.raw129step0 line 36
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical129 line 38
  8. def OAI.MUB6.Certificate.PairSemantics.raw130 line 47
  9. def OAI.MUB6.Certificate.PairSemantics.raw130step0 line 49
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical130 line 51
  11. def OAI.MUB6.Certificate.PairSemantics.raw131 line 60
  12. def OAI.MUB6.Certificate.PairSemantics.raw131step0 line 62
  13. def OAI.MUB6.Certificate.PairSemantics.raw131step1 line 64
  14. def OAI.MUB6.Certificate.PairSemantics.raw131step2 line 66
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical131 line 68
  16. def OAI.MUB6.Certificate.PairSemantics.raw132 line 85
  17. def OAI.MUB6.Certificate.PairSemantics.raw132step0 line 87
  18. def OAI.MUB6.Certificate.PairSemantics.raw132step1 line 89
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical132 line 91
  20. def OAI.MUB6.Certificate.PairSemantics.raw133 line 104
  21. def OAI.MUB6.Certificate.PairSemantics.raw133step0 line 106
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical133 line 108
  23. def OAI.MUB6.Certificate.PairSemantics.raw134 line 117
  24. def OAI.MUB6.Certificate.PairSemantics.raw134step0 line 119
  25. def OAI.MUB6.Certificate.PairSemantics.raw134step1 line 121
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical134 line 123
  27. def OAI.MUB6.Certificate.PairSemantics.raw135 line 136
  28. def OAI.MUB6.Certificate.PairSemantics.raw135step0 line 138
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical135 line 140
  30. def OAI.MUB6.Certificate.PairSemantics.raw136 line 149
  31. def OAI.MUB6.Certificate.PairSemantics.raw136step0 line 151
  32. def OAI.MUB6.Certificate.PairSemantics.raw136step1 line 153
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical136 line 155
  34. def OAI.MUB6.Certificate.PairSemantics.raw137 line 168
  35. def OAI.MUB6.Certificate.PairSemantics.raw137step0 line 170
  36. def OAI.MUB6.Certificate.PairSemantics.raw137step1 line 172
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical137 line 174
  38. def OAI.MUB6.Certificate.PairSemantics.raw138 line 187
  39. def OAI.MUB6.Certificate.PairSemantics.raw138step0 line 189
  40. def OAI.MUB6.Certificate.PairSemantics.raw138step1 line 191
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical138 line 193
  42. def OAI.MUB6.Certificate.PairSemantics.raw139 line 206
  43. def OAI.MUB6.Certificate.PairSemantics.raw139step0 line 208
  44. def OAI.MUB6.Certificate.PairSemantics.raw139step1 line 210
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical139 line 212
  46. def OAI.MUB6.Certificate.PairSemantics.raw140 line 225
  47. def OAI.MUB6.Certificate.PairSemantics.raw140step0 line 227
  48. def OAI.MUB6.Certificate.PairSemantics.raw140step1 line 229
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical140 line 231
  50. def OAI.MUB6.Certificate.PairSemantics.raw141 line 244
  51. def OAI.MUB6.Certificate.PairSemantics.raw141step0 line 246
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical141 line 248
  53. def OAI.MUB6.Certificate.PairSemantics.raw142 line 257
  54. def OAI.MUB6.Certificate.PairSemantics.raw142step0 line 259
  55. def OAI.MUB6.Certificate.PairSemantics.raw142step1 line 261
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical142 line 263
  57. def OAI.MUB6.Certificate.PairSemantics.raw143 line 276
  58. def OAI.MUB6.Certificate.PairSemantics.raw143step0 line 278
  59. def OAI.MUB6.Certificate.PairSemantics.raw143step1 line 280
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical143 line 282
  61. def OAI.MUB6.Certificate.PairSemantics.raw144 line 295
  62. def OAI.MUB6.Certificate.PairSemantics.raw144step0 line 297
  63. def OAI.MUB6.Certificate.PairSemantics.raw144step1 line 299
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical144 line 301
  65. def OAI.MUB6.Certificate.PairSemantics.raw145 line 314
  66. def OAI.MUB6.Certificate.PairSemantics.raw145step0 line 316
  67. def OAI.MUB6.Certificate.PairSemantics.raw145step1 line 318
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical145 line 320
  69. def OAI.MUB6.Certificate.PairSemantics.raw146 line 333
  70. def OAI.MUB6.Certificate.PairSemantics.raw146step0 line 335
  71. def OAI.MUB6.Certificate.PairSemantics.raw146step1 line 337
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical146 line 339
  73. def OAI.MUB6.Certificate.PairSemantics.raw147 line 352
  74. def OAI.MUB6.Certificate.PairSemantics.raw147step0 line 354
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical147 line 356
  76. def OAI.MUB6.Certificate.PairSemantics.raw148 line 365
  77. def OAI.MUB6.Certificate.PairSemantics.raw148step0 line 367
  78. def OAI.MUB6.Certificate.PairSemantics.raw148step1 line 369
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical148 line 371
  80. def OAI.MUB6.Certificate.PairSemantics.raw149 line 384
  81. def OAI.MUB6.Certificate.PairSemantics.raw149step0 line 386
  82. def OAI.MUB6.Certificate.PairSemantics.raw149step1 line 388
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical149 line 390
  84. def OAI.MUB6.Certificate.PairSemantics.raw150 line 403
  85. def OAI.MUB6.Certificate.PairSemantics.raw150step0 line 405
  86. def OAI.MUB6.Certificate.PairSemantics.raw150step1 line 407
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical150 line 409
  88. def OAI.MUB6.Certificate.PairSemantics.raw151 line 422
  89. def OAI.MUB6.Certificate.PairSemantics.raw151step0 line 424
  90. def OAI.MUB6.Certificate.PairSemantics.raw151step1 line 426
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical151 line 428
  92. def OAI.MUB6.Certificate.PairSemantics.raw152 line 441
  93. def OAI.MUB6.Certificate.PairSemantics.raw152step0 line 443
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical152 line 445
  95. def OAI.MUB6.Certificate.PairSemantics.raw153 line 454
  96. def OAI.MUB6.Certificate.PairSemantics.raw153step0 line 456
  97. def OAI.MUB6.Certificate.PairSemantics.raw153step1 line 458
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical153 line 460
  99. def OAI.MUB6.Certificate.PairSemantics.raw154 line 473
  100. def OAI.MUB6.Certificate.PairSemantics.raw154step0 line 475
  101. def OAI.MUB6.Certificate.PairSemantics.raw154step1 line 477
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical154 line 479
  103. def OAI.MUB6.Certificate.PairSemantics.raw155 line 492
  104. def OAI.MUB6.Certificate.PairSemantics.raw155step0 line 494
  105. def OAI.MUB6.Certificate.PairSemantics.raw155step1 line 496
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical155 line 498
  107. def OAI.MUB6.Certificate.PairSemantics.raw156 line 511
  108. def OAI.MUB6.Certificate.PairSemantics.raw156step0 line 513
  109. def OAI.MUB6.Certificate.PairSemantics.raw156step1 line 515
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical156 line 517
  111. def OAI.MUB6.Certificate.PairSemantics.raw157 line 530
  112. def OAI.MUB6.Certificate.PairSemantics.raw157step0 line 532
  113. def OAI.MUB6.Certificate.PairSemantics.raw157step1 line 534
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical157 line 536
  115. def OAI.MUB6.Certificate.PairSemantics.raw158 line 549
  116. def OAI.MUB6.Certificate.PairSemantics.raw158step0 line 551
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical158 line 553
  118. def OAI.MUB6.Certificate.PairSemantics.raw159 line 562
  119. def OAI.MUB6.Certificate.PairSemantics.raw159step0 line 564
  120. def OAI.MUB6.Certificate.PairSemantics.raw159step1 line 566
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical159 line 568