OAI/Analysis/MutuallyUnbiased/MixedMerge/Block8.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged256 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck256 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero256 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged257 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck257 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero257 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged258 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck258 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero258 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged259 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck259 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero259 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged260 line 48
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck260 line 50
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero260 line 52
  16. def OAI.MUB6.Certificate.MixedData.merged261 line 58
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck261 line 60
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero261 line 62
  19. def OAI.MUB6.Certificate.MixedData.merged262 line 68
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck262 line 70
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero262 line 72
  22. def OAI.MUB6.Certificate.MixedData.merged263 line 77
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck263 line 79
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero263 line 81
  25. def OAI.MUB6.Certificate.MixedData.merged264 line 86
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck264 line 88
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero264 line 90
  28. def OAI.MUB6.Certificate.MixedData.merged265 line 96
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck265 line 98
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero265 line 100
  31. def OAI.MUB6.Certificate.MixedData.merged266 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck266 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero266 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged267 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck267 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero267 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged268 line 124
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck268 line 126
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero268 line 128
  40. def OAI.MUB6.Certificate.MixedData.merged269 line 134
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck269 line 136
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero269 line 138
  43. def OAI.MUB6.Certificate.MixedData.merged270 line 144
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck270 line 146
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero270 line 148
  46. def OAI.MUB6.Certificate.MixedData.merged271 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck271 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero271 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged272 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck272 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero272 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged273 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck273 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero273 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged274 line 182
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck274 line 184
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero274 line 186
  58. def OAI.MUB6.Certificate.MixedData.merged275 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck275 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero275 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged276 line 200
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck276 line 202
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero276 line 204
  64. def OAI.MUB6.Certificate.MixedData.merged277 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck277 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero277 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged278 line 220
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck278 line 222
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero278 line 224
  70. def OAI.MUB6.Certificate.MixedData.merged279 line 230
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck279 line 232
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero279 line 234
  73. def OAI.MUB6.Certificate.MixedData.merged280 line 240
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck280 line 242
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero280 line 244
  76. def OAI.MUB6.Certificate.MixedData.merged281 line 249
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck281 line 251
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero281 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged282 line 258
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck282 line 260
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero282 line 262
  82. def OAI.MUB6.Certificate.MixedData.merged283 line 268
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck283 line 270
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero283 line 272
  85. def OAI.MUB6.Certificate.MixedData.merged284 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck284 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero284 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged285 line 286
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck285 line 288
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero285 line 290
  91. def OAI.MUB6.Certificate.MixedData.merged286 line 296
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck286 line 298
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero286 line 300
  94. def OAI.MUB6.Certificate.MixedData.merged287 line 306
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck287 line 308
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero287 line 310