OAI/Analysis/MutuallyUnbiased/MixedMerge/Block47.lean

GitHub source file

135 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1504 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1504 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1504 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1505 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1505 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1505 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged1506 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1506 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1506 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged1507 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1507 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1507 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged1508 line 48
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1508 line 50
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1508 line 52
  16. def OAI.MUB6.Certificate.MixedData.merged1509 line 58
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1509 line 60
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1509 line 62
  19. def OAI.MUB6.Certificate.MixedData.merged1510part0 line 68
  20. def OAI.MUB6.Certificate.MixedData.merged1510part1 line 70
  21. def OAI.MUB6.Certificate.MixedData.merged1510part2 line 72
  22. def OAI.MUB6.Certificate.MixedData.merged1510part3 line 74
  23. def OAI.MUB6.Certificate.MixedData.merged1510part4 line 76
  24. def OAI.MUB6.Certificate.MixedData.merged1510part5 line 78
  25. def OAI.MUB6.Certificate.MixedData.merged1510part6 line 80
  26. def OAI.MUB6.Certificate.MixedData.merged1510part7 line 82
  27. def OAI.MUB6.Certificate.MixedData.merged1510part8 line 84
  28. def OAI.MUB6.Certificate.MixedData.merged1510 line 86
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1510 line 88
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1510 line 90
  31. def OAI.MUB6.Certificate.MixedData.merged1511part0 line 96
  32. def OAI.MUB6.Certificate.MixedData.merged1511part1 line 98
  33. def OAI.MUB6.Certificate.MixedData.merged1511part2 line 100
  34. def OAI.MUB6.Certificate.MixedData.merged1511part3 line 102
  35. def OAI.MUB6.Certificate.MixedData.merged1511part4 line 104
  36. def OAI.MUB6.Certificate.MixedData.merged1511part5 line 106
  37. def OAI.MUB6.Certificate.MixedData.merged1511part6 line 108
  38. def OAI.MUB6.Certificate.MixedData.merged1511part7 line 110
  39. def OAI.MUB6.Certificate.MixedData.merged1511part8 line 112
  40. def OAI.MUB6.Certificate.MixedData.merged1511part9 line 114
  41. def OAI.MUB6.Certificate.MixedData.merged1511part10 line 116
  42. def OAI.MUB6.Certificate.MixedData.merged1511part11 line 118
  43. def OAI.MUB6.Certificate.MixedData.merged1511part12 line 120
  44. def OAI.MUB6.Certificate.MixedData.merged1511 line 122
  45. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1511 line 124
  46. theorem OAI.MUB6.Certificate.MixedData.mergedZero1511 line 126
  47. def OAI.MUB6.Certificate.MixedData.merged1512part0 line 132
  48. def OAI.MUB6.Certificate.MixedData.merged1512part1 line 134
  49. def OAI.MUB6.Certificate.MixedData.merged1512part2 line 136
  50. def OAI.MUB6.Certificate.MixedData.merged1512part3 line 138
  51. def OAI.MUB6.Certificate.MixedData.merged1512part4 line 140
  52. def OAI.MUB6.Certificate.MixedData.merged1512part5 line 142
  53. def OAI.MUB6.Certificate.MixedData.merged1512part6 line 144
  54. def OAI.MUB6.Certificate.MixedData.merged1512part7 line 146
  55. def OAI.MUB6.Certificate.MixedData.merged1512part8 line 148
  56. def OAI.MUB6.Certificate.MixedData.merged1512part9 line 150
  57. def OAI.MUB6.Certificate.MixedData.merged1512part10 line 152
  58. def OAI.MUB6.Certificate.MixedData.merged1512part11 line 154
  59. def OAI.MUB6.Certificate.MixedData.merged1512part12 line 156
  60. def OAI.MUB6.Certificate.MixedData.merged1512part13 line 158
  61. def OAI.MUB6.Certificate.MixedData.merged1512part14 line 160
  62. def OAI.MUB6.Certificate.MixedData.merged1512part15 line 162
  63. def OAI.MUB6.Certificate.MixedData.merged1512part16 line 164
  64. def OAI.MUB6.Certificate.MixedData.merged1512 line 166
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1512 line 168
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1512 line 170
  67. def OAI.MUB6.Certificate.MixedData.merged1513 line 176
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1513 line 178
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1513 line 180
  70. def OAI.MUB6.Certificate.MixedData.merged1514 line 185
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1514 line 187
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1514 line 189
  73. def OAI.MUB6.Certificate.MixedData.merged1515 line 194
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1515 line 196
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1515 line 198
  76. def OAI.MUB6.Certificate.MixedData.merged1516 line 204
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1516 line 206
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1516 line 208
  79. def OAI.MUB6.Certificate.MixedData.merged1517 line 213
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1517 line 215
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1517 line 217
  82. def OAI.MUB6.Certificate.MixedData.merged1518 line 222
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1518 line 224
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero1518 line 226
  85. def OAI.MUB6.Certificate.MixedData.merged1519 line 232
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1519 line 234
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero1519 line 236
  88. def OAI.MUB6.Certificate.MixedData.merged1520 line 242
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1520 line 244
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero1520 line 246
  91. def OAI.MUB6.Certificate.MixedData.merged1521 line 252
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1521 line 254
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero1521 line 256
  94. def OAI.MUB6.Certificate.MixedData.merged1522 line 261
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1522 line 263
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero1522 line 265
  97. def OAI.MUB6.Certificate.MixedData.merged1523 line 270
  98. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1523 line 272
  99. theorem OAI.MUB6.Certificate.MixedData.mergedZero1523 line 274
  100. def OAI.MUB6.Certificate.MixedData.merged1524 line 280
  101. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1524 line 282
  102. theorem OAI.MUB6.Certificate.MixedData.mergedZero1524 line 284
  103. def OAI.MUB6.Certificate.MixedData.merged1525 line 289
  104. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1525 line 291
  105. theorem OAI.MUB6.Certificate.MixedData.mergedZero1525 line 293
  106. def OAI.MUB6.Certificate.MixedData.merged1526 line 298
  107. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1526 line 300
  108. theorem OAI.MUB6.Certificate.MixedData.mergedZero1526 line 302
  109. def OAI.MUB6.Certificate.MixedData.merged1527 line 308
  110. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1527 line 310
  111. theorem OAI.MUB6.Certificate.MixedData.mergedZero1527 line 312
  112. def OAI.MUB6.Certificate.MixedData.merged1528 line 318
  113. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1528 line 320
  114. theorem OAI.MUB6.Certificate.MixedData.mergedZero1528 line 322
  115. def OAI.MUB6.Certificate.MixedData.merged1529 line 328
  116. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1529 line 330
  117. theorem OAI.MUB6.Certificate.MixedData.mergedZero1529 line 332
  118. def OAI.MUB6.Certificate.MixedData.merged1530 line 338
  119. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1530 line 340
  120. theorem OAI.MUB6.Certificate.MixedData.mergedZero1530 line 342
  121. def OAI.MUB6.Certificate.MixedData.merged1531 line 347
  122. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1531 line 349
  123. theorem OAI.MUB6.Certificate.MixedData.mergedZero1531 line 351
  124. def OAI.MUB6.Certificate.MixedData.merged1532 line 356
  125. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1532 line 358
  126. theorem OAI.MUB6.Certificate.MixedData.mergedZero1532 line 360
  127. def OAI.MUB6.Certificate.MixedData.merged1533 line 366
  128. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1533 line 368
  129. theorem OAI.MUB6.Certificate.MixedData.mergedZero1533 line 370
  130. def OAI.MUB6.Certificate.MixedData.merged1534 line 375
  131. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1534 line 377
  132. theorem OAI.MUB6.Certificate.MixedData.mergedZero1534 line 379
  133. def OAI.MUB6.Certificate.MixedData.merged1535 line 384
  134. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1535 line 386
  135. theorem OAI.MUB6.Certificate.MixedData.mergedZero1535 line 388