OAI/Analysis/MutuallyUnbiased/MixedMerge/Block40.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1280 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1280 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1280 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1281 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1281 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1281 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged1282 line 29
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1282 line 31
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1282 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged1283 line 39
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1283 line 41
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1283 line 43
  13. def OAI.MUB6.Certificate.MixedData.merged1284 line 49
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1284 line 51
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1284 line 53
  16. def OAI.MUB6.Certificate.MixedData.merged1285 line 59
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1285 line 61
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1285 line 63
  19. def OAI.MUB6.Certificate.MixedData.merged1286 line 68
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1286 line 70
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1286 line 72
  22. def OAI.MUB6.Certificate.MixedData.merged1287 line 77
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1287 line 79
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1287 line 81
  25. def OAI.MUB6.Certificate.MixedData.merged1288 line 87
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1288 line 89
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1288 line 91
  28. def OAI.MUB6.Certificate.MixedData.merged1289 line 96
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1289 line 98
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1289 line 100
  31. def OAI.MUB6.Certificate.MixedData.merged1290 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1290 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1290 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged1291 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1291 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1291 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged1292 line 125
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1292 line 127
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1292 line 129
  40. def OAI.MUB6.Certificate.MixedData.merged1293 line 135
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1293 line 137
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1293 line 139
  43. def OAI.MUB6.Certificate.MixedData.merged1294 line 144
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1294 line 146
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1294 line 148
  46. def OAI.MUB6.Certificate.MixedData.merged1295 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1295 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1295 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged1296 line 163
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1296 line 165
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1296 line 167
  52. def OAI.MUB6.Certificate.MixedData.merged1297 line 173
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1297 line 175
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1297 line 177
  55. def OAI.MUB6.Certificate.MixedData.merged1298 line 182
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1298 line 184
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1298 line 186
  58. def OAI.MUB6.Certificate.MixedData.merged1299 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1299 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1299 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged1300 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1300 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1300 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged1301 line 211
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1301 line 213
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1301 line 215
  67. def OAI.MUB6.Certificate.MixedData.merged1302 line 221
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1302 line 223
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1302 line 225
  70. def OAI.MUB6.Certificate.MixedData.merged1303 line 231
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1303 line 233
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1303 line 235
  73. def OAI.MUB6.Certificate.MixedData.merged1304 line 240
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1304 line 242
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1304 line 244
  76. def OAI.MUB6.Certificate.MixedData.merged1305 line 249
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1305 line 251
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1305 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged1306 line 259
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1306 line 261
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1306 line 263
  82. def OAI.MUB6.Certificate.MixedData.merged1307 line 268
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1307 line 270
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero1307 line 272
  85. def OAI.MUB6.Certificate.MixedData.merged1308 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1308 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero1308 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged1309 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1309 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero1309 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged1310 line 297
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1310 line 299
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero1310 line 301
  94. def OAI.MUB6.Certificate.MixedData.merged1311 line 307
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1311 line 309
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero1311 line 311