OAI/Analysis/MutuallyUnbiased/MixedMerge/Block75.lean

GitHub source file

187 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged2400 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2400 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero2400 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged2401 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2401 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero2401 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged2402 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2402 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero2402 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged2403 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2403 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero2403 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged2404 line 46
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2404 line 48
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero2404 line 50
  16. def OAI.MUB6.Certificate.MixedData.merged2405 line 56
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2405 line 58
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero2405 line 60
  19. def OAI.MUB6.Certificate.MixedData.merged2406 line 66
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2406 line 68
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero2406 line 70
  22. def OAI.MUB6.Certificate.MixedData.merged2407 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2407 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero2407 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged2408 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2408 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero2408 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged2409 line 94
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2409 line 96
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero2409 line 98
  31. def OAI.MUB6.Certificate.MixedData.merged2410 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2410 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero2410 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged2411 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2411 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero2411 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged2412 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2412 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero2412 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged2413 line 132
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2413 line 134
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero2413 line 136
  43. def OAI.MUB6.Certificate.MixedData.merged2414 line 142
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2414 line 144
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero2414 line 146
  46. def OAI.MUB6.Certificate.MixedData.merged2415 line 152
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2415 line 154
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero2415 line 156
  49. def OAI.MUB6.Certificate.MixedData.merged2416 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2416 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero2416 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged2417 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2417 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero2417 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged2418 line 182
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2418 line 184
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero2418 line 186
  58. def OAI.MUB6.Certificate.MixedData.merged2419 line 192
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2419 line 194
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero2419 line 196
  61. def OAI.MUB6.Certificate.MixedData.merged2420 line 202
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2420 line 204
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero2420 line 206
  64. def OAI.MUB6.Certificate.MixedData.merged2421part0 line 212
  65. def OAI.MUB6.Certificate.MixedData.merged2421part1 line 214
  66. def OAI.MUB6.Certificate.MixedData.merged2421part2 line 216
  67. def OAI.MUB6.Certificate.MixedData.merged2421part3 line 218
  68. def OAI.MUB6.Certificate.MixedData.merged2421part4 line 220
  69. def OAI.MUB6.Certificate.MixedData.merged2421part5 line 222
  70. def OAI.MUB6.Certificate.MixedData.merged2421part6 line 224
  71. def OAI.MUB6.Certificate.MixedData.merged2421part7 line 226
  72. def OAI.MUB6.Certificate.MixedData.merged2421part8 line 228
  73. def OAI.MUB6.Certificate.MixedData.merged2421part9 line 230
  74. def OAI.MUB6.Certificate.MixedData.merged2421part10 line 232
  75. def OAI.MUB6.Certificate.MixedData.merged2421part11 line 234
  76. def OAI.MUB6.Certificate.MixedData.merged2421part12 line 236
  77. def OAI.MUB6.Certificate.MixedData.merged2421part13 line 238
  78. def OAI.MUB6.Certificate.MixedData.merged2421part14 line 240
  79. def OAI.MUB6.Certificate.MixedData.merged2421part15 line 242
  80. def OAI.MUB6.Certificate.MixedData.merged2421part16 line 244
  81. def OAI.MUB6.Certificate.MixedData.merged2421part17 line 246
  82. def OAI.MUB6.Certificate.MixedData.merged2421part18 line 248
  83. def OAI.MUB6.Certificate.MixedData.merged2421part19 line 250
  84. def OAI.MUB6.Certificate.MixedData.merged2421part20 line 252
  85. def OAI.MUB6.Certificate.MixedData.merged2421part21 line 254
  86. def OAI.MUB6.Certificate.MixedData.merged2421part22 line 256
  87. def OAI.MUB6.Certificate.MixedData.merged2421part23 line 258
  88. def OAI.MUB6.Certificate.MixedData.merged2421part24 line 260
  89. def OAI.MUB6.Certificate.MixedData.merged2421part25 line 262
  90. def OAI.MUB6.Certificate.MixedData.merged2421 line 264
  91. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2421 line 266
  92. theorem OAI.MUB6.Certificate.MixedData.mergedZero2421 line 268
  93. def OAI.MUB6.Certificate.MixedData.merged2422part0 line 274
  94. def OAI.MUB6.Certificate.MixedData.merged2422part1 line 276
  95. def OAI.MUB6.Certificate.MixedData.merged2422part2 line 278
  96. def OAI.MUB6.Certificate.MixedData.merged2422part3 line 280
  97. def OAI.MUB6.Certificate.MixedData.merged2422part4 line 282
  98. def OAI.MUB6.Certificate.MixedData.merged2422part5 line 284
  99. def OAI.MUB6.Certificate.MixedData.merged2422part6 line 286
  100. def OAI.MUB6.Certificate.MixedData.merged2422part7 line 288
  101. def OAI.MUB6.Certificate.MixedData.merged2422part8 line 290
  102. def OAI.MUB6.Certificate.MixedData.merged2422part9 line 292
  103. def OAI.MUB6.Certificate.MixedData.merged2422part10 line 294
  104. def OAI.MUB6.Certificate.MixedData.merged2422part11 line 296
  105. def OAI.MUB6.Certificate.MixedData.merged2422part12 line 298
  106. def OAI.MUB6.Certificate.MixedData.merged2422part13 line 300
  107. def OAI.MUB6.Certificate.MixedData.merged2422part14 line 302
  108. def OAI.MUB6.Certificate.MixedData.merged2422part15 line 304
  109. def OAI.MUB6.Certificate.MixedData.merged2422part16 line 306
  110. def OAI.MUB6.Certificate.MixedData.merged2422part17 line 308
  111. def OAI.MUB6.Certificate.MixedData.merged2422part18 line 310
  112. def OAI.MUB6.Certificate.MixedData.merged2422part19 line 312
  113. def OAI.MUB6.Certificate.MixedData.merged2422part20 line 314
  114. def OAI.MUB6.Certificate.MixedData.merged2422part21 line 316
  115. def OAI.MUB6.Certificate.MixedData.merged2422part22 line 318
  116. def OAI.MUB6.Certificate.MixedData.merged2422part23 line 320
  117. def OAI.MUB6.Certificate.MixedData.merged2422part24 line 322
  118. def OAI.MUB6.Certificate.MixedData.merged2422part25 line 324
  119. def OAI.MUB6.Certificate.MixedData.merged2422part26 line 326
  120. def OAI.MUB6.Certificate.MixedData.merged2422part27 line 328
  121. def OAI.MUB6.Certificate.MixedData.merged2422part28 line 330
  122. def OAI.MUB6.Certificate.MixedData.merged2422part29 line 332
  123. def OAI.MUB6.Certificate.MixedData.merged2422part30 line 334
  124. def OAI.MUB6.Certificate.MixedData.merged2422part31 line 336
  125. def OAI.MUB6.Certificate.MixedData.merged2422part32 line 338
  126. def OAI.MUB6.Certificate.MixedData.merged2422 line 340
  127. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2422 line 342
  128. theorem OAI.MUB6.Certificate.MixedData.mergedZero2422 line 344
  129. def OAI.MUB6.Certificate.MixedData.merged2423part0 line 350
  130. def OAI.MUB6.Certificate.MixedData.merged2423part1 line 352
  131. def OAI.MUB6.Certificate.MixedData.merged2423part2 line 354
  132. def OAI.MUB6.Certificate.MixedData.merged2423part3 line 356
  133. def OAI.MUB6.Certificate.MixedData.merged2423part4 line 358
  134. def OAI.MUB6.Certificate.MixedData.merged2423part5 line 360
  135. def OAI.MUB6.Certificate.MixedData.merged2423part6 line 362
  136. def OAI.MUB6.Certificate.MixedData.merged2423part7 line 364
  137. def OAI.MUB6.Certificate.MixedData.merged2423part8 line 366
  138. def OAI.MUB6.Certificate.MixedData.merged2423part9 line 368
  139. def OAI.MUB6.Certificate.MixedData.merged2423part10 line 370
  140. def OAI.MUB6.Certificate.MixedData.merged2423part11 line 372
  141. def OAI.MUB6.Certificate.MixedData.merged2423part12 line 374
  142. def OAI.MUB6.Certificate.MixedData.merged2423part13 line 376
  143. def OAI.MUB6.Certificate.MixedData.merged2423part14 line 378
  144. def OAI.MUB6.Certificate.MixedData.merged2423part15 line 380
  145. def OAI.MUB6.Certificate.MixedData.merged2423part16 line 382
  146. def OAI.MUB6.Certificate.MixedData.merged2423part17 line 384
  147. def OAI.MUB6.Certificate.MixedData.merged2423part18 line 386
  148. def OAI.MUB6.Certificate.MixedData.merged2423part19 line 388
  149. def OAI.MUB6.Certificate.MixedData.merged2423part20 line 390
  150. def OAI.MUB6.Certificate.MixedData.merged2423part21 line 392
  151. def OAI.MUB6.Certificate.MixedData.merged2423part22 line 394
  152. def OAI.MUB6.Certificate.MixedData.merged2423part23 line 396
  153. def OAI.MUB6.Certificate.MixedData.merged2423 line 398
  154. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2423 line 400
  155. theorem OAI.MUB6.Certificate.MixedData.mergedZero2423 line 402
  156. def OAI.MUB6.Certificate.MixedData.merged2424 line 408
  157. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2424 line 410
  158. def OAI.MUB6.Certificate.MixedData.expr2424 line 412
  159. theorem OAI.MUB6.Certificate.MixedData.mergedEval2424 line 414
  160. def OAI.MUB6.Certificate.MixedData.merged2425 line 419
  161. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2425 line 421
  162. def OAI.MUB6.Certificate.MixedData.expr2425 line 423
  163. theorem OAI.MUB6.Certificate.MixedData.mergedEval2425 line 425
  164. def OAI.MUB6.Certificate.MixedData.merged2426 line 430
  165. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2426 line 432
  166. def OAI.MUB6.Certificate.MixedData.expr2426 line 434
  167. theorem OAI.MUB6.Certificate.MixedData.mergedEval2426 line 436
  168. def OAI.MUB6.Certificate.MixedData.merged2427 line 442
  169. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2427 line 444
  170. def OAI.MUB6.Certificate.MixedData.expr2427 line 446
  171. theorem OAI.MUB6.Certificate.MixedData.mergedEval2427 line 448
  172. def OAI.MUB6.Certificate.MixedData.merged2428 line 454
  173. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2428 line 456
  174. def OAI.MUB6.Certificate.MixedData.expr2428 line 458
  175. theorem OAI.MUB6.Certificate.MixedData.mergedEval2428 line 460
  176. def OAI.MUB6.Certificate.MixedData.merged2429 line 465
  177. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2429 line 467
  178. def OAI.MUB6.Certificate.MixedData.expr2429 line 469
  179. theorem OAI.MUB6.Certificate.MixedData.mergedEval2429 line 471
  180. def OAI.MUB6.Certificate.MixedData.merged2430 line 477
  181. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2430 line 479
  182. def OAI.MUB6.Certificate.MixedData.expr2430 line 481
  183. theorem OAI.MUB6.Certificate.MixedData.mergedEval2430 line 483
  184. def OAI.MUB6.Certificate.MixedData.merged2431 line 488
  185. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2431 line 490
  186. def OAI.MUB6.Certificate.MixedData.expr2431 line 492
  187. theorem OAI.MUB6.Certificate.MixedData.mergedEval2431 line 494