OAI/Analysis/MutuallyUnbiased/MixedMerge/Block70.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged2240 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2240 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero2240 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged2241 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2241 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero2241 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged2242 line 29
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2242 line 31
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero2242 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged2243 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2243 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero2243 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged2244 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2244 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero2244 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged2245 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2245 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero2245 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged2246 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2246 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero2246 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged2247 line 77
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2247 line 79
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero2247 line 81
  25. def OAI.MUB6.Certificate.MixedData.merged2248 line 87
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2248 line 89
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero2248 line 91
  28. def OAI.MUB6.Certificate.MixedData.merged2249 line 96
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2249 line 98
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero2249 line 100
  31. def OAI.MUB6.Certificate.MixedData.merged2250 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2250 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero2250 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged2251 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2251 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero2251 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged2252 line 124
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2252 line 126
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero2252 line 128
  40. def OAI.MUB6.Certificate.MixedData.merged2253 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2253 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero2253 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged2254 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2254 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero2254 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged2255 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2255 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero2255 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged2256 line 163
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2256 line 165
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero2256 line 167
  52. def OAI.MUB6.Certificate.MixedData.merged2257 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2257 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero2257 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged2258 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2258 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero2258 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged2259 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2259 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero2259 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged2260 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2260 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero2260 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged2261 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2261 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero2261 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged2262 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2262 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero2262 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged2263 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2263 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero2263 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged2264 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2264 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero2264 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged2265 line 249
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2265 line 251
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero2265 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged2266 line 259
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2266 line 261
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero2266 line 263
  82. def OAI.MUB6.Certificate.MixedData.merged2267 line 269
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2267 line 271
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero2267 line 273
  85. def OAI.MUB6.Certificate.MixedData.merged2268 line 279
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2268 line 281
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero2268 line 283
  88. def OAI.MUB6.Certificate.MixedData.merged2269 line 289
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2269 line 291
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero2269 line 293
  91. def OAI.MUB6.Certificate.MixedData.merged2270 line 298
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2270 line 300
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero2270 line 302
  94. def OAI.MUB6.Certificate.MixedData.merged2271 line 307
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2271 line 309
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero2271 line 311