OAI/Analysis/MutuallyUnbiased/MixedMerge/Block69.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged2208 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2208 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero2208 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged2209 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2209 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero2209 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged2210 line 29
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2210 line 31
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero2210 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged2211 line 39
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2211 line 41
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero2211 line 43
  13. def OAI.MUB6.Certificate.MixedData.merged2212 line 48
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2212 line 50
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero2212 line 52
  16. def OAI.MUB6.Certificate.MixedData.merged2213 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2213 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero2213 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged2214 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2214 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero2214 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged2215 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2215 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero2215 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged2216 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2216 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero2216 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged2217 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2217 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero2217 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged2218 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2218 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero2218 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged2219 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2219 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero2219 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged2220 line 124
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2220 line 126
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero2220 line 128
  40. def OAI.MUB6.Certificate.MixedData.merged2221 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2221 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero2221 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged2222 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2222 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero2222 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged2223 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2223 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero2223 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged2224 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2224 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero2224 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged2225 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2225 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero2225 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged2226 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2226 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero2226 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged2227 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2227 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero2227 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged2228 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2228 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero2228 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged2229 line 211
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2229 line 213
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero2229 line 215
  67. def OAI.MUB6.Certificate.MixedData.merged2230 line 221
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2230 line 223
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero2230 line 225
  70. def OAI.MUB6.Certificate.MixedData.merged2231 line 230
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2231 line 232
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero2231 line 234
  73. def OAI.MUB6.Certificate.MixedData.merged2232 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2232 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero2232 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged2233 line 249
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2233 line 251
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero2233 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged2234 line 258
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2234 line 260
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero2234 line 262
  82. def OAI.MUB6.Certificate.MixedData.merged2235 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2235 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero2235 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged2236 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2236 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero2236 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged2237 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2237 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero2237 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged2238 line 297
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2238 line 299
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero2238 line 301
  94. def OAI.MUB6.Certificate.MixedData.merged2239 line 306
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2239 line 308
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero2239 line 310