OAI/Analysis/MutuallyUnbiased/MixedMerge/Block37.lean

GitHub source file

175 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1184 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1184 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1184 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1185 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1185 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1185 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged1186 line 29
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1186 line 31
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1186 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged1187 line 39
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1187 line 41
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1187 line 43
  13. def OAI.MUB6.Certificate.MixedData.merged1188 line 48
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1188 line 50
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1188 line 52
  16. def OAI.MUB6.Certificate.MixedData.merged1189 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1189 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1189 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged1190 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1190 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1190 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged1191 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1191 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1191 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged1192 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1192 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1192 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged1193 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1193 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1193 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged1194 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1194 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1194 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged1195 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1195 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1195 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged1196 line 124
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1196 line 126
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1196 line 128
  40. def OAI.MUB6.Certificate.MixedData.merged1197 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1197 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1197 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged1198 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1198 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1198 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged1199 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1199 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1199 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged1200 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1200 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1200 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged1201 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1201 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1201 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged1202 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1202 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1202 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged1203 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1203 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1203 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged1204 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1204 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1204 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged1205 line 211
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1205 line 213
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1205 line 215
  67. def OAI.MUB6.Certificate.MixedData.merged1206 line 221
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1206 line 223
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1206 line 225
  70. def OAI.MUB6.Certificate.MixedData.merged1207part0 line 231
  71. def OAI.MUB6.Certificate.MixedData.merged1207part1 line 233
  72. def OAI.MUB6.Certificate.MixedData.merged1207part2 line 235
  73. def OAI.MUB6.Certificate.MixedData.merged1207part3 line 237
  74. def OAI.MUB6.Certificate.MixedData.merged1207part4 line 239
  75. def OAI.MUB6.Certificate.MixedData.merged1207part5 line 241
  76. def OAI.MUB6.Certificate.MixedData.merged1207part6 line 243
  77. def OAI.MUB6.Certificate.MixedData.merged1207part7 line 245
  78. def OAI.MUB6.Certificate.MixedData.merged1207part8 line 247
  79. def OAI.MUB6.Certificate.MixedData.merged1207part9 line 249
  80. def OAI.MUB6.Certificate.MixedData.merged1207 line 251
  81. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1207 line 253
  82. theorem OAI.MUB6.Certificate.MixedData.mergedZero1207 line 255
  83. def OAI.MUB6.Certificate.MixedData.merged1208part0 line 261
  84. def OAI.MUB6.Certificate.MixedData.merged1208part1 line 263
  85. def OAI.MUB6.Certificate.MixedData.merged1208part2 line 265
  86. def OAI.MUB6.Certificate.MixedData.merged1208part3 line 267
  87. def OAI.MUB6.Certificate.MixedData.merged1208part4 line 269
  88. def OAI.MUB6.Certificate.MixedData.merged1208part5 line 271
  89. def OAI.MUB6.Certificate.MixedData.merged1208part6 line 273
  90. def OAI.MUB6.Certificate.MixedData.merged1208part7 line 275
  91. def OAI.MUB6.Certificate.MixedData.merged1208part8 line 277
  92. def OAI.MUB6.Certificate.MixedData.merged1208part9 line 279
  93. def OAI.MUB6.Certificate.MixedData.merged1208part10 line 281
  94. def OAI.MUB6.Certificate.MixedData.merged1208part11 line 283
  95. def OAI.MUB6.Certificate.MixedData.merged1208part12 line 285
  96. def OAI.MUB6.Certificate.MixedData.merged1208part13 line 287
  97. def OAI.MUB6.Certificate.MixedData.merged1208part14 line 289
  98. def OAI.MUB6.Certificate.MixedData.merged1208part15 line 291
  99. def OAI.MUB6.Certificate.MixedData.merged1208part16 line 293
  100. def OAI.MUB6.Certificate.MixedData.merged1208 line 295
  101. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1208 line 297
  102. theorem OAI.MUB6.Certificate.MixedData.mergedZero1208 line 299
  103. def OAI.MUB6.Certificate.MixedData.merged1209part0 line 305
  104. def OAI.MUB6.Certificate.MixedData.merged1209part1 line 307
  105. def OAI.MUB6.Certificate.MixedData.merged1209part2 line 309
  106. def OAI.MUB6.Certificate.MixedData.merged1209part3 line 311
  107. def OAI.MUB6.Certificate.MixedData.merged1209part4 line 313
  108. def OAI.MUB6.Certificate.MixedData.merged1209part5 line 315
  109. def OAI.MUB6.Certificate.MixedData.merged1209part6 line 317
  110. def OAI.MUB6.Certificate.MixedData.merged1209part7 line 319
  111. def OAI.MUB6.Certificate.MixedData.merged1209part8 line 321
  112. def OAI.MUB6.Certificate.MixedData.merged1209part9 line 323
  113. def OAI.MUB6.Certificate.MixedData.merged1209part10 line 325
  114. def OAI.MUB6.Certificate.MixedData.merged1209part11 line 327
  115. def OAI.MUB6.Certificate.MixedData.merged1209part12 line 329
  116. def OAI.MUB6.Certificate.MixedData.merged1209part13 line 331
  117. def OAI.MUB6.Certificate.MixedData.merged1209part14 line 333
  118. def OAI.MUB6.Certificate.MixedData.merged1209part15 line 335
  119. def OAI.MUB6.Certificate.MixedData.merged1209part16 line 337
  120. def OAI.MUB6.Certificate.MixedData.merged1209part17 line 339
  121. def OAI.MUB6.Certificate.MixedData.merged1209part18 line 341
  122. def OAI.MUB6.Certificate.MixedData.merged1209part19 line 343
  123. def OAI.MUB6.Certificate.MixedData.merged1209part20 line 345
  124. def OAI.MUB6.Certificate.MixedData.merged1209part21 line 347
  125. def OAI.MUB6.Certificate.MixedData.merged1209part22 line 349
  126. def OAI.MUB6.Certificate.MixedData.merged1209part23 line 351
  127. def OAI.MUB6.Certificate.MixedData.merged1209part24 line 353
  128. def OAI.MUB6.Certificate.MixedData.merged1209part25 line 355
  129. def OAI.MUB6.Certificate.MixedData.merged1209 line 357
  130. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1209 line 359
  131. theorem OAI.MUB6.Certificate.MixedData.mergedZero1209 line 361
  132. def OAI.MUB6.Certificate.MixedData.merged1210part0 line 367
  133. def OAI.MUB6.Certificate.MixedData.merged1210part1 line 369
  134. def OAI.MUB6.Certificate.MixedData.merged1210part2 line 371
  135. def OAI.MUB6.Certificate.MixedData.merged1210part3 line 373
  136. def OAI.MUB6.Certificate.MixedData.merged1210part4 line 375
  137. def OAI.MUB6.Certificate.MixedData.merged1210part5 line 377
  138. def OAI.MUB6.Certificate.MixedData.merged1210part6 line 379
  139. def OAI.MUB6.Certificate.MixedData.merged1210part7 line 381
  140. def OAI.MUB6.Certificate.MixedData.merged1210part8 line 383
  141. def OAI.MUB6.Certificate.MixedData.merged1210part9 line 385
  142. def OAI.MUB6.Certificate.MixedData.merged1210part10 line 387
  143. def OAI.MUB6.Certificate.MixedData.merged1210part11 line 389
  144. def OAI.MUB6.Certificate.MixedData.merged1210part12 line 391
  145. def OAI.MUB6.Certificate.MixedData.merged1210part13 line 393
  146. def OAI.MUB6.Certificate.MixedData.merged1210part14 line 395
  147. def OAI.MUB6.Certificate.MixedData.merged1210part15 line 397
  148. def OAI.MUB6.Certificate.MixedData.merged1210part16 line 399
  149. def OAI.MUB6.Certificate.MixedData.merged1210part17 line 401
  150. def OAI.MUB6.Certificate.MixedData.merged1210part18 line 403
  151. def OAI.MUB6.Certificate.MixedData.merged1210part19 line 405
  152. def OAI.MUB6.Certificate.MixedData.merged1210part20 line 407
  153. def OAI.MUB6.Certificate.MixedData.merged1210part21 line 409
  154. def OAI.MUB6.Certificate.MixedData.merged1210part22 line 411
  155. def OAI.MUB6.Certificate.MixedData.merged1210part23 line 413
  156. def OAI.MUB6.Certificate.MixedData.merged1210part24 line 415
  157. def OAI.MUB6.Certificate.MixedData.merged1210part25 line 417
  158. def OAI.MUB6.Certificate.MixedData.merged1210 line 419
  159. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1210 line 421
  160. theorem OAI.MUB6.Certificate.MixedData.mergedZero1210 line 423
  161. def OAI.MUB6.Certificate.MixedData.merged1211 line 429
  162. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1211 line 431
  163. theorem OAI.MUB6.Certificate.MixedData.mergedZero1211 line 433
  164. def OAI.MUB6.Certificate.MixedData.merged1212 line 438
  165. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1212 line 440
  166. theorem OAI.MUB6.Certificate.MixedData.mergedZero1212 line 442
  167. def OAI.MUB6.Certificate.MixedData.merged1213 line 447
  168. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1213 line 449
  169. theorem OAI.MUB6.Certificate.MixedData.mergedZero1213 line 451
  170. def OAI.MUB6.Certificate.MixedData.merged1214 line 457
  171. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1214 line 459
  172. theorem OAI.MUB6.Certificate.MixedData.mergedZero1214 line 461
  173. def OAI.MUB6.Certificate.MixedData.merged1215 line 466
  174. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1215 line 468
  175. theorem OAI.MUB6.Certificate.MixedData.mergedZero1215 line 470