OAI/Analysis/MutuallyUnbiased/MixedMerge/Block11.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged352 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck352 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero352 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged353 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck353 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero353 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged354 line 29
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck354 line 31
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero354 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged355 line 39
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck355 line 41
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero355 line 43
  13. def OAI.MUB6.Certificate.MixedData.merged356 line 49
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck356 line 51
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero356 line 53
  16. def OAI.MUB6.Certificate.MixedData.merged357 line 58
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck357 line 60
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero357 line 62
  19. def OAI.MUB6.Certificate.MixedData.merged358 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck358 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero358 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged359 line 77
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck359 line 79
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero359 line 81
  25. def OAI.MUB6.Certificate.MixedData.merged360 line 86
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck360 line 88
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero360 line 90
  28. def OAI.MUB6.Certificate.MixedData.merged361 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck361 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero361 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged362 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck362 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero362 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged363 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck363 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero363 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged364 line 125
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck364 line 127
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero364 line 129
  40. def OAI.MUB6.Certificate.MixedData.merged365 line 134
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck365 line 136
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero365 line 138
  43. def OAI.MUB6.Certificate.MixedData.merged366 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck366 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero366 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged367 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck367 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero367 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged368 line 163
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck368 line 165
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero368 line 167
  52. def OAI.MUB6.Certificate.MixedData.merged369 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck369 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero369 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged370 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck370 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero370 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged371 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck371 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero371 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged372 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck372 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero372 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged373 line 211
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck373 line 213
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero373 line 215
  67. def OAI.MUB6.Certificate.MixedData.merged374 line 221
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck374 line 223
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero374 line 225
  70. def OAI.MUB6.Certificate.MixedData.merged375 line 231
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck375 line 233
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero375 line 235
  73. def OAI.MUB6.Certificate.MixedData.merged376 line 241
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck376 line 243
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero376 line 245
  76. def OAI.MUB6.Certificate.MixedData.merged377 line 250
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck377 line 252
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero377 line 254
  79. def OAI.MUB6.Certificate.MixedData.merged378 line 259
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck378 line 261
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero378 line 263
  82. def OAI.MUB6.Certificate.MixedData.merged379 line 269
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck379 line 271
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero379 line 273
  85. def OAI.MUB6.Certificate.MixedData.merged380 line 278
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck380 line 280
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero380 line 282
  88. def OAI.MUB6.Certificate.MixedData.merged381 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck381 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero381 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged382 line 297
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck382 line 299
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero382 line 301
  94. def OAI.MUB6.Certificate.MixedData.merged383 line 307
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck383 line 309
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero383 line 311