OAI/Analysis/MutuallyUnbiased/MixedMerge/Block18.lean

GitHub source file

152 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged576 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck576 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero576 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged577 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck577 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero577 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged578 line 27
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck578 line 29
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero578 line 31
  10. def OAI.MUB6.Certificate.MixedData.merged579 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck579 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero579 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged580 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck580 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero580 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged581 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck581 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero581 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged582 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck582 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero582 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged583 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck583 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero583 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged584 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck584 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero584 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged585 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck585 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero585 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged586 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck586 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero586 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged587 line 113
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck587 line 115
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero587 line 117
  37. def OAI.MUB6.Certificate.MixedData.merged588 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck588 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero588 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged589 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck589 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero589 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged590 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck590 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero590 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged591 line 152
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck591 line 154
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero591 line 156
  49. def OAI.MUB6.Certificate.MixedData.merged592 line 161
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck592 line 163
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero592 line 165
  52. def OAI.MUB6.Certificate.MixedData.merged593 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck593 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero593 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged594 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck594 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero594 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged595 line 190
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck595 line 192
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero595 line 194
  61. def OAI.MUB6.Certificate.MixedData.merged596 line 199
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck596 line 201
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero596 line 203
  64. def OAI.MUB6.Certificate.MixedData.merged597 line 209
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck597 line 211
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero597 line 213
  67. def OAI.MUB6.Certificate.MixedData.merged598 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck598 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero598 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged599 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck599 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero599 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged600 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck600 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero600 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged601part0 line 249
  77. def OAI.MUB6.Certificate.MixedData.merged601part1 line 251
  78. def OAI.MUB6.Certificate.MixedData.merged601part2 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged601part3 line 255
  80. def OAI.MUB6.Certificate.MixedData.merged601part4 line 257
  81. def OAI.MUB6.Certificate.MixedData.merged601part5 line 259
  82. def OAI.MUB6.Certificate.MixedData.merged601part6 line 261
  83. def OAI.MUB6.Certificate.MixedData.merged601part7 line 263
  84. def OAI.MUB6.Certificate.MixedData.merged601 line 265
  85. theorem OAI.MUB6.Certificate.MixedData.mergeCheck601 line 267
  86. theorem OAI.MUB6.Certificate.MixedData.mergedZero601 line 269
  87. def OAI.MUB6.Certificate.MixedData.merged602part0 line 275
  88. def OAI.MUB6.Certificate.MixedData.merged602part1 line 277
  89. def OAI.MUB6.Certificate.MixedData.merged602part2 line 279
  90. def OAI.MUB6.Certificate.MixedData.merged602part3 line 281
  91. def OAI.MUB6.Certificate.MixedData.merged602part4 line 283
  92. def OAI.MUB6.Certificate.MixedData.merged602part5 line 285
  93. def OAI.MUB6.Certificate.MixedData.merged602part6 line 287
  94. def OAI.MUB6.Certificate.MixedData.merged602part7 line 289
  95. def OAI.MUB6.Certificate.MixedData.merged602part8 line 291
  96. def OAI.MUB6.Certificate.MixedData.merged602part9 line 293
  97. def OAI.MUB6.Certificate.MixedData.merged602part10 line 295
  98. def OAI.MUB6.Certificate.MixedData.merged602part11 line 297
  99. def OAI.MUB6.Certificate.MixedData.merged602part12 line 299
  100. def OAI.MUB6.Certificate.MixedData.merged602 line 301
  101. theorem OAI.MUB6.Certificate.MixedData.mergeCheck602 line 303
  102. theorem OAI.MUB6.Certificate.MixedData.mergedZero602 line 305
  103. def OAI.MUB6.Certificate.MixedData.merged603part0 line 311
  104. def OAI.MUB6.Certificate.MixedData.merged603part1 line 313
  105. def OAI.MUB6.Certificate.MixedData.merged603part2 line 315
  106. def OAI.MUB6.Certificate.MixedData.merged603part3 line 317
  107. def OAI.MUB6.Certificate.MixedData.merged603part4 line 319
  108. def OAI.MUB6.Certificate.MixedData.merged603part5 line 321
  109. def OAI.MUB6.Certificate.MixedData.merged603part6 line 323
  110. def OAI.MUB6.Certificate.MixedData.merged603part7 line 325
  111. def OAI.MUB6.Certificate.MixedData.merged603part8 line 327
  112. def OAI.MUB6.Certificate.MixedData.merged603part9 line 329
  113. def OAI.MUB6.Certificate.MixedData.merged603part10 line 331
  114. def OAI.MUB6.Certificate.MixedData.merged603part11 line 333
  115. def OAI.MUB6.Certificate.MixedData.merged603part12 line 335
  116. def OAI.MUB6.Certificate.MixedData.merged603part13 line 337
  117. def OAI.MUB6.Certificate.MixedData.merged603part14 line 339
  118. def OAI.MUB6.Certificate.MixedData.merged603part15 line 341
  119. def OAI.MUB6.Certificate.MixedData.merged603 line 343
  120. theorem OAI.MUB6.Certificate.MixedData.mergeCheck603 line 345
  121. theorem OAI.MUB6.Certificate.MixedData.mergedZero603 line 347
  122. def OAI.MUB6.Certificate.MixedData.merged604part0 line 353
  123. def OAI.MUB6.Certificate.MixedData.merged604part1 line 355
  124. def OAI.MUB6.Certificate.MixedData.merged604part2 line 357
  125. def OAI.MUB6.Certificate.MixedData.merged604part3 line 359
  126. def OAI.MUB6.Certificate.MixedData.merged604part4 line 361
  127. def OAI.MUB6.Certificate.MixedData.merged604part5 line 363
  128. def OAI.MUB6.Certificate.MixedData.merged604part6 line 365
  129. def OAI.MUB6.Certificate.MixedData.merged604part7 line 367
  130. def OAI.MUB6.Certificate.MixedData.merged604part8 line 369
  131. def OAI.MUB6.Certificate.MixedData.merged604part9 line 371
  132. def OAI.MUB6.Certificate.MixedData.merged604part10 line 373
  133. def OAI.MUB6.Certificate.MixedData.merged604part11 line 375
  134. def OAI.MUB6.Certificate.MixedData.merged604part12 line 377
  135. def OAI.MUB6.Certificate.MixedData.merged604part13 line 379
  136. def OAI.MUB6.Certificate.MixedData.merged604part14 line 381
  137. def OAI.MUB6.Certificate.MixedData.merged604part15 line 383
  138. def OAI.MUB6.Certificate.MixedData.merged604part16 line 385
  139. def OAI.MUB6.Certificate.MixedData.merged604part17 line 387
  140. def OAI.MUB6.Certificate.MixedData.merged604part18 line 389
  141. def OAI.MUB6.Certificate.MixedData.merged604 line 391
  142. theorem OAI.MUB6.Certificate.MixedData.mergeCheck604 line 393
  143. theorem OAI.MUB6.Certificate.MixedData.mergedZero604 line 395
  144. def OAI.MUB6.Certificate.MixedData.merged605 line 401
  145. theorem OAI.MUB6.Certificate.MixedData.mergeCheck605 line 403
  146. theorem OAI.MUB6.Certificate.MixedData.mergedZero605 line 405
  147. def OAI.MUB6.Certificate.MixedData.merged606 line 410
  148. theorem OAI.MUB6.Certificate.MixedData.mergeCheck606 line 412
  149. theorem OAI.MUB6.Certificate.MixedData.mergedZero606 line 414
  150. def OAI.MUB6.Certificate.MixedData.merged607 line 419
  151. theorem OAI.MUB6.Certificate.MixedData.mergeCheck607 line 421
  152. theorem OAI.MUB6.Certificate.MixedData.mergedZero607 line 423