OAI/Analysis/MutuallyUnbiased/MixedMerge/Block71.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged2272 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2272 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero2272 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged2273 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2273 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero2273 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged2274 line 27
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2274 line 29
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero2274 line 31
  10. def OAI.MUB6.Certificate.MixedData.merged2275 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2275 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero2275 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged2276 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2276 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero2276 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged2277 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2277 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero2277 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged2278 line 66
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2278 line 68
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero2278 line 70
  22. def OAI.MUB6.Certificate.MixedData.merged2279 line 75
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2279 line 77
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero2279 line 79
  25. def OAI.MUB6.Certificate.MixedData.merged2280 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2280 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero2280 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged2281 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2281 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero2281 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged2282 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2282 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero2282 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged2283 line 113
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2283 line 115
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero2283 line 117
  37. def OAI.MUB6.Certificate.MixedData.merged2284 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2284 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero2284 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged2285 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2285 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero2285 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged2286 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2286 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero2286 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged2287 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2287 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero2287 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged2288 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2288 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero2288 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged2289 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2289 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero2289 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged2290 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2290 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero2290 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged2291 line 190
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2291 line 192
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero2291 line 194
  61. def OAI.MUB6.Certificate.MixedData.merged2292 line 199
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2292 line 201
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero2292 line 203
  64. def OAI.MUB6.Certificate.MixedData.merged2293 line 209
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2293 line 211
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero2293 line 213
  67. def OAI.MUB6.Certificate.MixedData.merged2294 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2294 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero2294 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged2295 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2295 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero2295 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged2296 line 238
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2296 line 240
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero2296 line 242
  76. def OAI.MUB6.Certificate.MixedData.merged2297 line 247
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2297 line 249
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero2297 line 251
  79. def OAI.MUB6.Certificate.MixedData.merged2298 line 257
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2298 line 259
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero2298 line 261
  82. def OAI.MUB6.Certificate.MixedData.merged2299 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2299 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero2299 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged2300 line 276
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2300 line 278
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero2300 line 280
  88. def OAI.MUB6.Certificate.MixedData.merged2301 line 285
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2301 line 287
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero2301 line 289
  91. def OAI.MUB6.Certificate.MixedData.merged2302 line 295
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2302 line 297
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero2302 line 299
  94. def OAI.MUB6.Certificate.MixedData.merged2303 line 305
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2303 line 307
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero2303 line 309