OAI/Analysis/MutuallyUnbiased/MixedMerge/Block73.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged2336 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2336 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero2336 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged2337 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2337 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero2337 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged2338 line 27
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2338 line 29
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero2338 line 31
  10. def OAI.MUB6.Certificate.MixedData.merged2339 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2339 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero2339 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged2340 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2340 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero2340 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged2341 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2341 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero2341 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged2342 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2342 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero2342 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged2343 line 77
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2343 line 79
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero2343 line 81
  25. def OAI.MUB6.Certificate.MixedData.merged2344 line 87
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2344 line 89
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero2344 line 91
  28. def OAI.MUB6.Certificate.MixedData.merged2345 line 96
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2345 line 98
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero2345 line 100
  31. def OAI.MUB6.Certificate.MixedData.merged2346 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2346 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero2346 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged2347 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2347 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero2347 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged2348 line 124
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2348 line 126
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero2348 line 128
  40. def OAI.MUB6.Certificate.MixedData.merged2349 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2349 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero2349 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged2350 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2350 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero2350 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged2351 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2351 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero2351 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged2352 line 163
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2352 line 165
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero2352 line 167
  52. def OAI.MUB6.Certificate.MixedData.merged2353 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2353 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero2353 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged2354 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2354 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero2354 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged2355 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2355 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero2355 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged2356 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2356 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero2356 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged2357 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2357 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero2357 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged2358 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2358 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero2358 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged2359 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2359 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero2359 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged2360 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2360 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero2360 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged2361 line 249
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2361 line 251
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero2361 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged2362 line 259
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2362 line 261
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero2362 line 263
  82. def OAI.MUB6.Certificate.MixedData.merged2363 line 268
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2363 line 270
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero2363 line 272
  85. def OAI.MUB6.Certificate.MixedData.merged2364 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2364 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero2364 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged2365 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2365 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero2365 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged2366 line 296
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2366 line 298
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero2366 line 300
  94. def OAI.MUB6.Certificate.MixedData.merged2367 line 305
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2367 line 307
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero2367 line 309