OAI/Analysis/MutuallyUnbiased/MixedMerge/Block38.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1216 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1216 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1216 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1217 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1217 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1217 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged1218 line 29
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1218 line 31
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1218 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged1219 line 39
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1219 line 41
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1219 line 43
  13. def OAI.MUB6.Certificate.MixedData.merged1220 line 48
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1220 line 50
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1220 line 52
  16. def OAI.MUB6.Certificate.MixedData.merged1221 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1221 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1221 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged1222 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1222 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1222 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged1223 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1223 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1223 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged1224 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1224 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1224 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged1225 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1225 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1225 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged1226 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1226 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1226 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged1227 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1227 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1227 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged1228 line 125
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1228 line 127
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1228 line 129
  40. def OAI.MUB6.Certificate.MixedData.merged1229 line 134
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1229 line 136
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1229 line 138
  43. def OAI.MUB6.Certificate.MixedData.merged1230 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1230 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1230 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged1231 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1231 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1231 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged1232 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1232 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1232 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged1233 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1233 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1233 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged1234 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1234 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1234 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged1235 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1235 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1235 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged1236 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1236 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1236 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged1237 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1237 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1237 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged1238 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1238 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1238 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged1239 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1239 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1239 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged1240 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1240 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1240 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged1241 line 248
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1241 line 250
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1241 line 252
  79. def OAI.MUB6.Certificate.MixedData.merged1242 line 257
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1242 line 259
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1242 line 261
  82. def OAI.MUB6.Certificate.MixedData.merged1243 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1243 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero1243 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged1244 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1244 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero1244 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged1245 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1245 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero1245 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged1246 line 297
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1246 line 299
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero1246 line 301
  94. def OAI.MUB6.Certificate.MixedData.merged1247 line 307
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1247 line 309
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero1247 line 311