OAI/Analysis/MutuallyUnbiased/MixedMerge/Block14.lean

GitHub source file

113 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged448 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck448 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero448 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged449 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck449 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero449 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged450part0 line 29
  8. def OAI.MUB6.Certificate.MixedData.merged450part1 line 31
  9. def OAI.MUB6.Certificate.MixedData.merged450part2 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged450part3 line 35
  11. def OAI.MUB6.Certificate.MixedData.merged450part4 line 37
  12. def OAI.MUB6.Certificate.MixedData.merged450part5 line 39
  13. def OAI.MUB6.Certificate.MixedData.merged450part6 line 41
  14. def OAI.MUB6.Certificate.MixedData.merged450 line 43
  15. theorem OAI.MUB6.Certificate.MixedData.mergeCheck450 line 45
  16. theorem OAI.MUB6.Certificate.MixedData.mergedZero450 line 47
  17. def OAI.MUB6.Certificate.MixedData.merged451part0 line 53
  18. def OAI.MUB6.Certificate.MixedData.merged451part1 line 55
  19. def OAI.MUB6.Certificate.MixedData.merged451part2 line 57
  20. def OAI.MUB6.Certificate.MixedData.merged451part3 line 59
  21. def OAI.MUB6.Certificate.MixedData.merged451part4 line 61
  22. def OAI.MUB6.Certificate.MixedData.merged451part5 line 63
  23. def OAI.MUB6.Certificate.MixedData.merged451part6 line 65
  24. def OAI.MUB6.Certificate.MixedData.merged451part7 line 67
  25. def OAI.MUB6.Certificate.MixedData.merged451part8 line 69
  26. def OAI.MUB6.Certificate.MixedData.merged451part9 line 71
  27. def OAI.MUB6.Certificate.MixedData.merged451 line 73
  28. theorem OAI.MUB6.Certificate.MixedData.mergeCheck451 line 75
  29. theorem OAI.MUB6.Certificate.MixedData.mergedZero451 line 77
  30. def OAI.MUB6.Certificate.MixedData.merged452 line 83
  31. theorem OAI.MUB6.Certificate.MixedData.mergeCheck452 line 85
  32. theorem OAI.MUB6.Certificate.MixedData.mergedZero452 line 87
  33. def OAI.MUB6.Certificate.MixedData.merged453 line 92
  34. theorem OAI.MUB6.Certificate.MixedData.mergeCheck453 line 94
  35. theorem OAI.MUB6.Certificate.MixedData.mergedZero453 line 96
  36. def OAI.MUB6.Certificate.MixedData.merged454 line 101
  37. theorem OAI.MUB6.Certificate.MixedData.mergeCheck454 line 103
  38. theorem OAI.MUB6.Certificate.MixedData.mergedZero454 line 105
  39. def OAI.MUB6.Certificate.MixedData.merged455 line 111
  40. theorem OAI.MUB6.Certificate.MixedData.mergeCheck455 line 113
  41. theorem OAI.MUB6.Certificate.MixedData.mergedZero455 line 115
  42. def OAI.MUB6.Certificate.MixedData.merged456 line 120
  43. theorem OAI.MUB6.Certificate.MixedData.mergeCheck456 line 122
  44. theorem OAI.MUB6.Certificate.MixedData.mergedZero456 line 124
  45. def OAI.MUB6.Certificate.MixedData.merged457 line 129
  46. theorem OAI.MUB6.Certificate.MixedData.mergeCheck457 line 131
  47. theorem OAI.MUB6.Certificate.MixedData.mergedZero457 line 133
  48. def OAI.MUB6.Certificate.MixedData.merged458 line 139
  49. theorem OAI.MUB6.Certificate.MixedData.mergeCheck458 line 141
  50. theorem OAI.MUB6.Certificate.MixedData.mergedZero458 line 143
  51. def OAI.MUB6.Certificate.MixedData.merged459 line 149
  52. theorem OAI.MUB6.Certificate.MixedData.mergeCheck459 line 151
  53. theorem OAI.MUB6.Certificate.MixedData.mergedZero459 line 153
  54. def OAI.MUB6.Certificate.MixedData.merged460 line 159
  55. theorem OAI.MUB6.Certificate.MixedData.mergeCheck460 line 161
  56. theorem OAI.MUB6.Certificate.MixedData.mergedZero460 line 163
  57. def OAI.MUB6.Certificate.MixedData.merged461 line 168
  58. theorem OAI.MUB6.Certificate.MixedData.mergeCheck461 line 170
  59. theorem OAI.MUB6.Certificate.MixedData.mergedZero461 line 172
  60. def OAI.MUB6.Certificate.MixedData.merged462 line 177
  61. theorem OAI.MUB6.Certificate.MixedData.mergeCheck462 line 179
  62. theorem OAI.MUB6.Certificate.MixedData.mergedZero462 line 181
  63. def OAI.MUB6.Certificate.MixedData.merged463 line 187
  64. theorem OAI.MUB6.Certificate.MixedData.mergeCheck463 line 189
  65. theorem OAI.MUB6.Certificate.MixedData.mergedZero463 line 191
  66. def OAI.MUB6.Certificate.MixedData.merged464 line 197
  67. theorem OAI.MUB6.Certificate.MixedData.mergeCheck464 line 199
  68. theorem OAI.MUB6.Certificate.MixedData.mergedZero464 line 201
  69. def OAI.MUB6.Certificate.MixedData.merged465 line 206
  70. theorem OAI.MUB6.Certificate.MixedData.mergeCheck465 line 208
  71. theorem OAI.MUB6.Certificate.MixedData.mergedZero465 line 210
  72. def OAI.MUB6.Certificate.MixedData.merged466 line 215
  73. theorem OAI.MUB6.Certificate.MixedData.mergeCheck466 line 217
  74. theorem OAI.MUB6.Certificate.MixedData.mergedZero466 line 219
  75. def OAI.MUB6.Certificate.MixedData.merged467 line 225
  76. theorem OAI.MUB6.Certificate.MixedData.mergeCheck467 line 227
  77. theorem OAI.MUB6.Certificate.MixedData.mergedZero467 line 229
  78. def OAI.MUB6.Certificate.MixedData.merged468 line 235
  79. theorem OAI.MUB6.Certificate.MixedData.mergeCheck468 line 237
  80. theorem OAI.MUB6.Certificate.MixedData.mergedZero468 line 239
  81. def OAI.MUB6.Certificate.MixedData.merged469 line 245
  82. theorem OAI.MUB6.Certificate.MixedData.mergeCheck469 line 247
  83. theorem OAI.MUB6.Certificate.MixedData.mergedZero469 line 249
  84. def OAI.MUB6.Certificate.MixedData.merged470 line 255
  85. theorem OAI.MUB6.Certificate.MixedData.mergeCheck470 line 257
  86. theorem OAI.MUB6.Certificate.MixedData.mergedZero470 line 259
  87. def OAI.MUB6.Certificate.MixedData.merged471 line 264
  88. theorem OAI.MUB6.Certificate.MixedData.mergeCheck471 line 266
  89. theorem OAI.MUB6.Certificate.MixedData.mergedZero471 line 268
  90. def OAI.MUB6.Certificate.MixedData.merged472 line 273
  91. theorem OAI.MUB6.Certificate.MixedData.mergeCheck472 line 275
  92. theorem OAI.MUB6.Certificate.MixedData.mergedZero472 line 277
  93. def OAI.MUB6.Certificate.MixedData.merged473 line 283
  94. theorem OAI.MUB6.Certificate.MixedData.mergeCheck473 line 285
  95. theorem OAI.MUB6.Certificate.MixedData.mergedZero473 line 287
  96. def OAI.MUB6.Certificate.MixedData.merged474 line 292
  97. theorem OAI.MUB6.Certificate.MixedData.mergeCheck474 line 294
  98. theorem OAI.MUB6.Certificate.MixedData.mergedZero474 line 296
  99. def OAI.MUB6.Certificate.MixedData.merged475 line 301
  100. theorem OAI.MUB6.Certificate.MixedData.mergeCheck475 line 303
  101. theorem OAI.MUB6.Certificate.MixedData.mergedZero475 line 305
  102. def OAI.MUB6.Certificate.MixedData.merged476 line 311
  103. theorem OAI.MUB6.Certificate.MixedData.mergeCheck476 line 313
  104. theorem OAI.MUB6.Certificate.MixedData.mergedZero476 line 315
  105. def OAI.MUB6.Certificate.MixedData.merged477 line 321
  106. theorem OAI.MUB6.Certificate.MixedData.mergeCheck477 line 323
  107. theorem OAI.MUB6.Certificate.MixedData.mergedZero477 line 325
  108. def OAI.MUB6.Certificate.MixedData.merged478 line 331
  109. theorem OAI.MUB6.Certificate.MixedData.mergeCheck478 line 333
  110. theorem OAI.MUB6.Certificate.MixedData.mergedZero478 line 335
  111. def OAI.MUB6.Certificate.MixedData.merged479 line 340
  112. theorem OAI.MUB6.Certificate.MixedData.mergeCheck479 line 342
  113. theorem OAI.MUB6.Certificate.MixedData.mergedZero479 line 344