OAI/Analysis/MutuallyUnbiased/MixedMerge/Block56.lean

GitHub source file

169 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1792 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1792 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1792 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1793 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1793 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1793 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged1794 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1794 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1794 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged1795 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1795 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1795 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged1796 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1796 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1796 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged1797 line 56
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1797 line 58
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1797 line 60
  19. def OAI.MUB6.Certificate.MixedData.merged1798 line 65
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1798 line 67
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1798 line 69
  22. def OAI.MUB6.Certificate.MixedData.merged1799 line 75
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1799 line 77
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1799 line 79
  25. def OAI.MUB6.Certificate.MixedData.merged1800 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1800 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1800 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged1801 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1801 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1801 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged1802 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1802 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1802 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged1803 line 113
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1803 line 115
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1803 line 117
  37. def OAI.MUB6.Certificate.MixedData.merged1804 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1804 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1804 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged1805 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1805 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1805 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged1806 line 142
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1806 line 144
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1806 line 146
  46. def OAI.MUB6.Certificate.MixedData.merged1807 line 151
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1807 line 153
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1807 line 155
  49. def OAI.MUB6.Certificate.MixedData.merged1808 line 161
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1808 line 163
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1808 line 165
  52. def OAI.MUB6.Certificate.MixedData.merged1809 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1809 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1809 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged1810 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1810 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1810 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged1811 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1811 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1811 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged1812part0 line 201
  62. def OAI.MUB6.Certificate.MixedData.merged1812part1 line 203
  63. def OAI.MUB6.Certificate.MixedData.merged1812part2 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged1812part3 line 207
  65. def OAI.MUB6.Certificate.MixedData.merged1812part4 line 209
  66. def OAI.MUB6.Certificate.MixedData.merged1812part5 line 211
  67. def OAI.MUB6.Certificate.MixedData.merged1812part6 line 213
  68. def OAI.MUB6.Certificate.MixedData.merged1812part7 line 215
  69. def OAI.MUB6.Certificate.MixedData.merged1812 line 217
  70. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1812 line 219
  71. theorem OAI.MUB6.Certificate.MixedData.mergedZero1812 line 221
  72. def OAI.MUB6.Certificate.MixedData.merged1813part0 line 227
  73. def OAI.MUB6.Certificate.MixedData.merged1813part1 line 229
  74. def OAI.MUB6.Certificate.MixedData.merged1813part2 line 231
  75. def OAI.MUB6.Certificate.MixedData.merged1813part3 line 233
  76. def OAI.MUB6.Certificate.MixedData.merged1813part4 line 235
  77. def OAI.MUB6.Certificate.MixedData.merged1813part5 line 237
  78. def OAI.MUB6.Certificate.MixedData.merged1813part6 line 239
  79. def OAI.MUB6.Certificate.MixedData.merged1813part7 line 241
  80. def OAI.MUB6.Certificate.MixedData.merged1813part8 line 243
  81. def OAI.MUB6.Certificate.MixedData.merged1813part9 line 245
  82. def OAI.MUB6.Certificate.MixedData.merged1813part10 line 247
  83. def OAI.MUB6.Certificate.MixedData.merged1813part11 line 249
  84. def OAI.MUB6.Certificate.MixedData.merged1813part12 line 251
  85. def OAI.MUB6.Certificate.MixedData.merged1813part13 line 253
  86. def OAI.MUB6.Certificate.MixedData.merged1813part14 line 255
  87. def OAI.MUB6.Certificate.MixedData.merged1813part15 line 257
  88. def OAI.MUB6.Certificate.MixedData.merged1813 line 259
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1813 line 261
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero1813 line 263
  91. def OAI.MUB6.Certificate.MixedData.merged1814part0 line 269
  92. def OAI.MUB6.Certificate.MixedData.merged1814part1 line 271
  93. def OAI.MUB6.Certificate.MixedData.merged1814part2 line 273
  94. def OAI.MUB6.Certificate.MixedData.merged1814part3 line 275
  95. def OAI.MUB6.Certificate.MixedData.merged1814part4 line 277
  96. def OAI.MUB6.Certificate.MixedData.merged1814part5 line 279
  97. def OAI.MUB6.Certificate.MixedData.merged1814part6 line 281
  98. def OAI.MUB6.Certificate.MixedData.merged1814part7 line 283
  99. def OAI.MUB6.Certificate.MixedData.merged1814part8 line 285
  100. def OAI.MUB6.Certificate.MixedData.merged1814part9 line 287
  101. def OAI.MUB6.Certificate.MixedData.merged1814part10 line 289
  102. def OAI.MUB6.Certificate.MixedData.merged1814part11 line 291
  103. def OAI.MUB6.Certificate.MixedData.merged1814part12 line 293
  104. def OAI.MUB6.Certificate.MixedData.merged1814part13 line 295
  105. def OAI.MUB6.Certificate.MixedData.merged1814part14 line 297
  106. def OAI.MUB6.Certificate.MixedData.merged1814part15 line 299
  107. def OAI.MUB6.Certificate.MixedData.merged1814part16 line 301
  108. def OAI.MUB6.Certificate.MixedData.merged1814part17 line 303
  109. def OAI.MUB6.Certificate.MixedData.merged1814part18 line 305
  110. def OAI.MUB6.Certificate.MixedData.merged1814part19 line 307
  111. def OAI.MUB6.Certificate.MixedData.merged1814part20 line 309
  112. def OAI.MUB6.Certificate.MixedData.merged1814part21 line 311
  113. def OAI.MUB6.Certificate.MixedData.merged1814 line 313
  114. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1814 line 315
  115. theorem OAI.MUB6.Certificate.MixedData.mergedZero1814 line 317
  116. def OAI.MUB6.Certificate.MixedData.merged1815part0 line 323
  117. def OAI.MUB6.Certificate.MixedData.merged1815part1 line 325
  118. def OAI.MUB6.Certificate.MixedData.merged1815part2 line 327
  119. def OAI.MUB6.Certificate.MixedData.merged1815part3 line 329
  120. def OAI.MUB6.Certificate.MixedData.merged1815part4 line 331
  121. def OAI.MUB6.Certificate.MixedData.merged1815part5 line 333
  122. def OAI.MUB6.Certificate.MixedData.merged1815part6 line 335
  123. def OAI.MUB6.Certificate.MixedData.merged1815part7 line 337
  124. def OAI.MUB6.Certificate.MixedData.merged1815part8 line 339
  125. def OAI.MUB6.Certificate.MixedData.merged1815part9 line 341
  126. def OAI.MUB6.Certificate.MixedData.merged1815part10 line 343
  127. def OAI.MUB6.Certificate.MixedData.merged1815part11 line 345
  128. def OAI.MUB6.Certificate.MixedData.merged1815part12 line 347
  129. def OAI.MUB6.Certificate.MixedData.merged1815part13 line 349
  130. def OAI.MUB6.Certificate.MixedData.merged1815part14 line 351
  131. def OAI.MUB6.Certificate.MixedData.merged1815part15 line 353
  132. def OAI.MUB6.Certificate.MixedData.merged1815part16 line 355
  133. def OAI.MUB6.Certificate.MixedData.merged1815part17 line 357
  134. def OAI.MUB6.Certificate.MixedData.merged1815part18 line 359
  135. def OAI.MUB6.Certificate.MixedData.merged1815part19 line 361
  136. def OAI.MUB6.Certificate.MixedData.merged1815part20 line 363
  137. def OAI.MUB6.Certificate.MixedData.merged1815part21 line 365
  138. def OAI.MUB6.Certificate.MixedData.merged1815part22 line 367
  139. def OAI.MUB6.Certificate.MixedData.merged1815part23 line 369
  140. def OAI.MUB6.Certificate.MixedData.merged1815part24 line 371
  141. def OAI.MUB6.Certificate.MixedData.merged1815part25 line 373
  142. def OAI.MUB6.Certificate.MixedData.merged1815part26 line 375
  143. def OAI.MUB6.Certificate.MixedData.merged1815 line 377
  144. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1815 line 379
  145. theorem OAI.MUB6.Certificate.MixedData.mergedZero1815 line 381
  146. def OAI.MUB6.Certificate.MixedData.merged1816 line 387
  147. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1816 line 389
  148. theorem OAI.MUB6.Certificate.MixedData.mergedZero1816 line 391
  149. def OAI.MUB6.Certificate.MixedData.merged1817 line 396
  150. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1817 line 398
  151. theorem OAI.MUB6.Certificate.MixedData.mergedZero1817 line 400
  152. def OAI.MUB6.Certificate.MixedData.merged1818 line 405
  153. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1818 line 407
  154. theorem OAI.MUB6.Certificate.MixedData.mergedZero1818 line 409
  155. def OAI.MUB6.Certificate.MixedData.merged1819 line 415
  156. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1819 line 417
  157. theorem OAI.MUB6.Certificate.MixedData.mergedZero1819 line 419
  158. def OAI.MUB6.Certificate.MixedData.merged1820 line 424
  159. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1820 line 426
  160. theorem OAI.MUB6.Certificate.MixedData.mergedZero1820 line 428
  161. def OAI.MUB6.Certificate.MixedData.merged1821 line 433
  162. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1821 line 435
  163. theorem OAI.MUB6.Certificate.MixedData.mergedZero1821 line 437
  164. def OAI.MUB6.Certificate.MixedData.merged1822 line 443
  165. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1822 line 445
  166. theorem OAI.MUB6.Certificate.MixedData.mergedZero1822 line 447
  167. def OAI.MUB6.Certificate.MixedData.merged1823 line 453
  168. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1823 line 455
  169. theorem OAI.MUB6.Certificate.MixedData.mergedZero1823 line 457