OAI/Analysis/MutuallyUnbiased/MixedMerge/Block41.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1312 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1312 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1312 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1313 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1313 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1313 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged1314 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1314 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1314 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged1315 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1315 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1315 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged1316 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1316 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1316 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged1317 line 56
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1317 line 58
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1317 line 60
  19. def OAI.MUB6.Certificate.MixedData.merged1318 line 66
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1318 line 68
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1318 line 70
  22. def OAI.MUB6.Certificate.MixedData.merged1319 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1319 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1319 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged1320 line 86
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1320 line 88
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1320 line 90
  28. def OAI.MUB6.Certificate.MixedData.merged1321 line 96
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1321 line 98
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1321 line 100
  31. def OAI.MUB6.Certificate.MixedData.merged1322 line 106
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1322 line 108
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1322 line 110
  34. def OAI.MUB6.Certificate.MixedData.merged1323 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1323 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1323 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged1324 line 124
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1324 line 126
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1324 line 128
  40. def OAI.MUB6.Certificate.MixedData.merged1325 line 134
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1325 line 136
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1325 line 138
  43. def OAI.MUB6.Certificate.MixedData.merged1326 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1326 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1326 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged1327 line 152
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1327 line 154
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1327 line 156
  49. def OAI.MUB6.Certificate.MixedData.merged1328 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1328 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1328 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged1329 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1329 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1329 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged1330 line 182
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1330 line 184
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1330 line 186
  58. def OAI.MUB6.Certificate.MixedData.merged1331 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1331 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1331 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged1332 line 200
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1332 line 202
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1332 line 204
  64. def OAI.MUB6.Certificate.MixedData.merged1333 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1333 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1333 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged1334 line 220
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1334 line 222
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1334 line 224
  70. def OAI.MUB6.Certificate.MixedData.merged1335 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1335 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1335 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged1336 line 238
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1336 line 240
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1336 line 242
  76. def OAI.MUB6.Certificate.MixedData.merged1337 line 248
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1337 line 250
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1337 line 252
  79. def OAI.MUB6.Certificate.MixedData.merged1338 line 258
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1338 line 260
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1338 line 262
  82. def OAI.MUB6.Certificate.MixedData.merged1339 line 268
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1339 line 270
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero1339 line 272
  85. def OAI.MUB6.Certificate.MixedData.merged1340 line 278
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1340 line 280
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero1340 line 282
  88. def OAI.MUB6.Certificate.MixedData.merged1341 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1341 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero1341 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged1342 line 296
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1342 line 298
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero1342 line 300
  94. def OAI.MUB6.Certificate.MixedData.merged1343 line 306
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1343 line 308
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero1343 line 310