OAI/Analysis/MutuallyUnbiased/MixedMerge/Block39.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1248 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1248 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1248 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1249 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1249 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1249 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged1250 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1250 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1250 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged1251 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1251 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1251 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged1252 line 46
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1252 line 48
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1252 line 50
  16. def OAI.MUB6.Certificate.MixedData.merged1253 line 56
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1253 line 58
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1253 line 60
  19. def OAI.MUB6.Certificate.MixedData.merged1254 line 66
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1254 line 68
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1254 line 70
  22. def OAI.MUB6.Certificate.MixedData.merged1255 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1255 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1255 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged1256 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1256 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1256 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged1257 line 94
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1257 line 96
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1257 line 98
  31. def OAI.MUB6.Certificate.MixedData.merged1258 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1258 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1258 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged1259 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1259 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1259 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged1260 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1260 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1260 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged1261 line 132
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1261 line 134
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1261 line 136
  43. def OAI.MUB6.Certificate.MixedData.merged1262 line 142
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1262 line 144
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1262 line 146
  46. def OAI.MUB6.Certificate.MixedData.merged1263 line 152
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1263 line 154
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1263 line 156
  49. def OAI.MUB6.Certificate.MixedData.merged1264 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1264 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1264 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged1265 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1265 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1265 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged1266 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1266 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1266 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged1267 line 190
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1267 line 192
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1267 line 194
  61. def OAI.MUB6.Certificate.MixedData.merged1268 line 200
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1268 line 202
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1268 line 204
  64. def OAI.MUB6.Certificate.MixedData.merged1269 line 209
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1269 line 211
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1269 line 213
  67. def OAI.MUB6.Certificate.MixedData.merged1270 line 218
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1270 line 220
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1270 line 222
  70. def OAI.MUB6.Certificate.MixedData.merged1271 line 228
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1271 line 230
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1271 line 232
  73. def OAI.MUB6.Certificate.MixedData.merged1272 line 238
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1272 line 240
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1272 line 242
  76. def OAI.MUB6.Certificate.MixedData.merged1273 line 248
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1273 line 250
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1273 line 252
  79. def OAI.MUB6.Certificate.MixedData.merged1274 line 257
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1274 line 259
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1274 line 261
  82. def OAI.MUB6.Certificate.MixedData.merged1275 line 266
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1275 line 268
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero1275 line 270
  85. def OAI.MUB6.Certificate.MixedData.merged1276 line 276
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1276 line 278
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero1276 line 280
  88. def OAI.MUB6.Certificate.MixedData.merged1277 line 286
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1277 line 288
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero1277 line 290
  91. def OAI.MUB6.Certificate.MixedData.merged1278 line 295
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1278 line 297
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero1278 line 299
  94. def OAI.MUB6.Certificate.MixedData.merged1279 line 304
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1279 line 306
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero1279 line 308