OAI/Analysis/MutuallyUnbiased/MixedMerge/Block76.lean

GitHub source file

154 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged2432 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2432 line 11
  3. def OAI.MUB6.Certificate.MixedData.expr2432 line 13
  4. theorem OAI.MUB6.Certificate.MixedData.mergedEval2432 line 15
  5. def OAI.MUB6.Certificate.MixedData.merged2433part0 line 21
  6. def OAI.MUB6.Certificate.MixedData.merged2433part1 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged2433part2 line 25
  8. def OAI.MUB6.Certificate.MixedData.merged2433part3 line 27
  9. def OAI.MUB6.Certificate.MixedData.merged2433part4 line 29
  10. def OAI.MUB6.Certificate.MixedData.merged2433part5 line 31
  11. def OAI.MUB6.Certificate.MixedData.merged2433part6 line 33
  12. def OAI.MUB6.Certificate.MixedData.merged2433part7 line 35
  13. def OAI.MUB6.Certificate.MixedData.merged2433part8 line 37
  14. def OAI.MUB6.Certificate.MixedData.merged2433part9 line 39
  15. def OAI.MUB6.Certificate.MixedData.merged2433part10 line 41
  16. def OAI.MUB6.Certificate.MixedData.merged2433 line 43
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2433 line 45
  18. def OAI.MUB6.Certificate.MixedData.expr2433 line 47
  19. theorem OAI.MUB6.Certificate.MixedData.mergedEval2433 line 49
  20. def OAI.MUB6.Certificate.MixedData.merged2434 line 55
  21. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2434 line 57
  22. def OAI.MUB6.Certificate.MixedData.expr2434 line 59
  23. theorem OAI.MUB6.Certificate.MixedData.mergedEval2434 line 61
  24. def OAI.MUB6.Certificate.MixedData.merged2435 line 66
  25. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2435 line 68
  26. def OAI.MUB6.Certificate.MixedData.expr2435 line 70
  27. theorem OAI.MUB6.Certificate.MixedData.mergedEval2435 line 72
  28. def OAI.MUB6.Certificate.MixedData.merged2436 line 78
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2436 line 80
  30. def OAI.MUB6.Certificate.MixedData.expr2436 line 82
  31. theorem OAI.MUB6.Certificate.MixedData.mergedEval2436 line 84
  32. def OAI.MUB6.Certificate.MixedData.merged2437 line 89
  33. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2437 line 91
  34. def OAI.MUB6.Certificate.MixedData.expr2437 line 93
  35. theorem OAI.MUB6.Certificate.MixedData.mergedEval2437 line 95
  36. def OAI.MUB6.Certificate.MixedData.merged2438 line 101
  37. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2438 line 103
  38. def OAI.MUB6.Certificate.MixedData.expr2438 line 105
  39. theorem OAI.MUB6.Certificate.MixedData.mergedEval2438 line 107
  40. def OAI.MUB6.Certificate.MixedData.merged2439 line 113
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2439 line 115
  42. def OAI.MUB6.Certificate.MixedData.expr2439 line 117
  43. theorem OAI.MUB6.Certificate.MixedData.mergedEval2439 line 119
  44. def OAI.MUB6.Certificate.MixedData.merged2440 line 124
  45. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2440 line 126
  46. def OAI.MUB6.Certificate.MixedData.expr2440 line 128
  47. theorem OAI.MUB6.Certificate.MixedData.mergedEval2440 line 130
  48. def OAI.MUB6.Certificate.MixedData.merged2441 line 136
  49. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2441 line 138
  50. def OAI.MUB6.Certificate.MixedData.expr2441 line 140
  51. theorem OAI.MUB6.Certificate.MixedData.mergedEval2441 line 142
  52. def OAI.MUB6.Certificate.MixedData.merged2442 line 147
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2442 line 149
  54. def OAI.MUB6.Certificate.MixedData.expr2442 line 151
  55. theorem OAI.MUB6.Certificate.MixedData.mergedEval2442 line 153
  56. def OAI.MUB6.Certificate.MixedData.merged2443 line 159
  57. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2443 line 161
  58. def OAI.MUB6.Certificate.MixedData.expr2443 line 163
  59. theorem OAI.MUB6.Certificate.MixedData.mergedEval2443 line 165
  60. def OAI.MUB6.Certificate.MixedData.merged2444part0 line 171
  61. def OAI.MUB6.Certificate.MixedData.merged2444part1 line 173
  62. def OAI.MUB6.Certificate.MixedData.merged2444part2 line 175
  63. def OAI.MUB6.Certificate.MixedData.merged2444part3 line 177
  64. def OAI.MUB6.Certificate.MixedData.merged2444part4 line 179
  65. def OAI.MUB6.Certificate.MixedData.merged2444part5 line 181
  66. def OAI.MUB6.Certificate.MixedData.merged2444part6 line 183
  67. def OAI.MUB6.Certificate.MixedData.merged2444part7 line 185
  68. def OAI.MUB6.Certificate.MixedData.merged2444part8 line 187
  69. def OAI.MUB6.Certificate.MixedData.merged2444part9 line 189
  70. def OAI.MUB6.Certificate.MixedData.merged2444part10 line 191
  71. def OAI.MUB6.Certificate.MixedData.merged2444part11 line 193
  72. def OAI.MUB6.Certificate.MixedData.merged2444 line 195
  73. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2444 line 197
  74. def OAI.MUB6.Certificate.MixedData.expr2444 line 199
  75. theorem OAI.MUB6.Certificate.MixedData.mergedEval2444 line 201
  76. def OAI.MUB6.Certificate.MixedData.merged2445part0 line 207
  77. def OAI.MUB6.Certificate.MixedData.merged2445part1 line 209
  78. def OAI.MUB6.Certificate.MixedData.merged2445part2 line 211
  79. def OAI.MUB6.Certificate.MixedData.merged2445part3 line 213
  80. def OAI.MUB6.Certificate.MixedData.merged2445part4 line 215
  81. def OAI.MUB6.Certificate.MixedData.merged2445part5 line 217
  82. def OAI.MUB6.Certificate.MixedData.merged2445part6 line 219
  83. def OAI.MUB6.Certificate.MixedData.merged2445part7 line 221
  84. def OAI.MUB6.Certificate.MixedData.merged2445part8 line 223
  85. def OAI.MUB6.Certificate.MixedData.merged2445part9 line 225
  86. def OAI.MUB6.Certificate.MixedData.merged2445part10 line 227
  87. def OAI.MUB6.Certificate.MixedData.merged2445part11 line 229
  88. def OAI.MUB6.Certificate.MixedData.merged2445part12 line 231
  89. def OAI.MUB6.Certificate.MixedData.merged2445part13 line 233
  90. def OAI.MUB6.Certificate.MixedData.merged2445part14 line 235
  91. def OAI.MUB6.Certificate.MixedData.merged2445part15 line 237
  92. def OAI.MUB6.Certificate.MixedData.merged2445part16 line 239
  93. def OAI.MUB6.Certificate.MixedData.merged2445part17 line 241
  94. def OAI.MUB6.Certificate.MixedData.merged2445part18 line 243
  95. def OAI.MUB6.Certificate.MixedData.merged2445part19 line 245
  96. def OAI.MUB6.Certificate.MixedData.merged2445part20 line 247
  97. def OAI.MUB6.Certificate.MixedData.merged2445part21 line 249
  98. def OAI.MUB6.Certificate.MixedData.merged2445part22 line 251
  99. def OAI.MUB6.Certificate.MixedData.merged2445 line 253
  100. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2445 line 255
  101. def OAI.MUB6.Certificate.MixedData.expr2445 line 257
  102. theorem OAI.MUB6.Certificate.MixedData.mergedEval2445 line 259
  103. def OAI.MUB6.Certificate.MixedData.merged2446 line 265
  104. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2446 line 267
  105. def OAI.MUB6.Certificate.MixedData.expr2446 line 269
  106. theorem OAI.MUB6.Certificate.MixedData.mergedEval2446 line 271
  107. def OAI.MUB6.Certificate.MixedData.merged2447 line 276
  108. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2447 line 278
  109. def OAI.MUB6.Certificate.MixedData.expr2447 line 280
  110. theorem OAI.MUB6.Certificate.MixedData.mergedEval2447 line 282
  111. def OAI.MUB6.Certificate.MixedData.merged2448 line 288
  112. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2448 line 290
  113. def OAI.MUB6.Certificate.MixedData.expr2448 line 292
  114. theorem OAI.MUB6.Certificate.MixedData.mergedEval2448 line 294
  115. def OAI.MUB6.Certificate.MixedData.merged2449 line 299
  116. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2449 line 301
  117. def OAI.MUB6.Certificate.MixedData.expr2449 line 303
  118. theorem OAI.MUB6.Certificate.MixedData.mergedEval2449 line 305
  119. def OAI.MUB6.Certificate.MixedData.merged2450 line 311
  120. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2450 line 313
  121. def OAI.MUB6.Certificate.MixedData.expr2450 line 315
  122. theorem OAI.MUB6.Certificate.MixedData.mergedEval2450 line 317
  123. def OAI.MUB6.Certificate.MixedData.merged2451 line 323
  124. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2451 line 325
  125. def OAI.MUB6.Certificate.MixedData.expr2451 line 327
  126. theorem OAI.MUB6.Certificate.MixedData.mergedEval2451 line 329
  127. def OAI.MUB6.Certificate.MixedData.merged2452part0 line 334
  128. def OAI.MUB6.Certificate.MixedData.merged2452part1 line 336
  129. def OAI.MUB6.Certificate.MixedData.merged2452part2 line 338
  130. def OAI.MUB6.Certificate.MixedData.merged2452part3 line 340
  131. def OAI.MUB6.Certificate.MixedData.merged2452part4 line 342
  132. def OAI.MUB6.Certificate.MixedData.merged2452part5 line 344
  133. def OAI.MUB6.Certificate.MixedData.merged2452part6 line 346
  134. def OAI.MUB6.Certificate.MixedData.merged2452part7 line 348
  135. def OAI.MUB6.Certificate.MixedData.merged2452part8 line 350
  136. def OAI.MUB6.Certificate.MixedData.merged2452part9 line 352
  137. def OAI.MUB6.Certificate.MixedData.merged2452part10 line 354
  138. def OAI.MUB6.Certificate.MixedData.merged2452part11 line 356
  139. def OAI.MUB6.Certificate.MixedData.merged2452part12 line 358
  140. def OAI.MUB6.Certificate.MixedData.merged2452part13 line 360
  141. def OAI.MUB6.Certificate.MixedData.merged2452part14 line 362
  142. def OAI.MUB6.Certificate.MixedData.merged2452part15 line 364
  143. def OAI.MUB6.Certificate.MixedData.merged2452part16 line 366
  144. def OAI.MUB6.Certificate.MixedData.merged2452part17 line 368
  145. def OAI.MUB6.Certificate.MixedData.merged2452part18 line 370
  146. def OAI.MUB6.Certificate.MixedData.merged2452part19 line 372
  147. def OAI.MUB6.Certificate.MixedData.merged2452part20 line 374
  148. def OAI.MUB6.Certificate.MixedData.merged2452part21 line 376
  149. def OAI.MUB6.Certificate.MixedData.merged2452part22 line 378
  150. def OAI.MUB6.Certificate.MixedData.merged2452part23 line 380
  151. def OAI.MUB6.Certificate.MixedData.merged2452 line 382
  152. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2452 line 384
  153. def OAI.MUB6.Certificate.MixedData.expr2452 line 386
  154. theorem OAI.MUB6.Certificate.MixedData.mergedEval2452 line 388