OAI/Analysis/MutuallyUnbiased/MixedMerge/Block66.lean

GitHub source file

157 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged2112 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2112 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero2112 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged2113 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2113 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero2113 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged2114part0 line 29
  8. def OAI.MUB6.Certificate.MixedData.merged2114part1 line 31
  9. def OAI.MUB6.Certificate.MixedData.merged2114part2 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged2114part3 line 35
  11. def OAI.MUB6.Certificate.MixedData.merged2114part4 line 37
  12. def OAI.MUB6.Certificate.MixedData.merged2114part5 line 39
  13. def OAI.MUB6.Certificate.MixedData.merged2114part6 line 41
  14. def OAI.MUB6.Certificate.MixedData.merged2114 line 43
  15. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2114 line 45
  16. theorem OAI.MUB6.Certificate.MixedData.mergedZero2114 line 47
  17. def OAI.MUB6.Certificate.MixedData.merged2115part0 line 53
  18. def OAI.MUB6.Certificate.MixedData.merged2115part1 line 55
  19. def OAI.MUB6.Certificate.MixedData.merged2115part2 line 57
  20. def OAI.MUB6.Certificate.MixedData.merged2115part3 line 59
  21. def OAI.MUB6.Certificate.MixedData.merged2115part4 line 61
  22. def OAI.MUB6.Certificate.MixedData.merged2115part5 line 63
  23. def OAI.MUB6.Certificate.MixedData.merged2115part6 line 65
  24. def OAI.MUB6.Certificate.MixedData.merged2115part7 line 67
  25. def OAI.MUB6.Certificate.MixedData.merged2115part8 line 69
  26. def OAI.MUB6.Certificate.MixedData.merged2115part9 line 71
  27. def OAI.MUB6.Certificate.MixedData.merged2115part10 line 73
  28. def OAI.MUB6.Certificate.MixedData.merged2115 line 75
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2115 line 77
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero2115 line 79
  31. def OAI.MUB6.Certificate.MixedData.merged2116part0 line 85
  32. def OAI.MUB6.Certificate.MixedData.merged2116part1 line 87
  33. def OAI.MUB6.Certificate.MixedData.merged2116part2 line 89
  34. def OAI.MUB6.Certificate.MixedData.merged2116part3 line 91
  35. def OAI.MUB6.Certificate.MixedData.merged2116part4 line 93
  36. def OAI.MUB6.Certificate.MixedData.merged2116part5 line 95
  37. def OAI.MUB6.Certificate.MixedData.merged2116part6 line 97
  38. def OAI.MUB6.Certificate.MixedData.merged2116part7 line 99
  39. def OAI.MUB6.Certificate.MixedData.merged2116part8 line 101
  40. def OAI.MUB6.Certificate.MixedData.merged2116part9 line 103
  41. def OAI.MUB6.Certificate.MixedData.merged2116part10 line 105
  42. def OAI.MUB6.Certificate.MixedData.merged2116part11 line 107
  43. def OAI.MUB6.Certificate.MixedData.merged2116part12 line 109
  44. def OAI.MUB6.Certificate.MixedData.merged2116part13 line 111
  45. def OAI.MUB6.Certificate.MixedData.merged2116part14 line 113
  46. def OAI.MUB6.Certificate.MixedData.merged2116part15 line 115
  47. def OAI.MUB6.Certificate.MixedData.merged2116part16 line 117
  48. def OAI.MUB6.Certificate.MixedData.merged2116part17 line 119
  49. def OAI.MUB6.Certificate.MixedData.merged2116 line 121
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2116 line 123
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero2116 line 125
  52. def OAI.MUB6.Certificate.MixedData.merged2117part0 line 131
  53. def OAI.MUB6.Certificate.MixedData.merged2117part1 line 133
  54. def OAI.MUB6.Certificate.MixedData.merged2117part2 line 135
  55. def OAI.MUB6.Certificate.MixedData.merged2117part3 line 137
  56. def OAI.MUB6.Certificate.MixedData.merged2117part4 line 139
  57. def OAI.MUB6.Certificate.MixedData.merged2117part5 line 141
  58. def OAI.MUB6.Certificate.MixedData.merged2117part6 line 143
  59. def OAI.MUB6.Certificate.MixedData.merged2117part7 line 145
  60. def OAI.MUB6.Certificate.MixedData.merged2117part8 line 147
  61. def OAI.MUB6.Certificate.MixedData.merged2117part9 line 149
  62. def OAI.MUB6.Certificate.MixedData.merged2117part10 line 151
  63. def OAI.MUB6.Certificate.MixedData.merged2117part11 line 153
  64. def OAI.MUB6.Certificate.MixedData.merged2117part12 line 155
  65. def OAI.MUB6.Certificate.MixedData.merged2117part13 line 157
  66. def OAI.MUB6.Certificate.MixedData.merged2117part14 line 159
  67. def OAI.MUB6.Certificate.MixedData.merged2117part15 line 161
  68. def OAI.MUB6.Certificate.MixedData.merged2117part16 line 163
  69. def OAI.MUB6.Certificate.MixedData.merged2117part17 line 165
  70. def OAI.MUB6.Certificate.MixedData.merged2117part18 line 167
  71. def OAI.MUB6.Certificate.MixedData.merged2117part19 line 169
  72. def OAI.MUB6.Certificate.MixedData.merged2117part20 line 171
  73. def OAI.MUB6.Certificate.MixedData.merged2117part21 line 173
  74. def OAI.MUB6.Certificate.MixedData.merged2117part22 line 175
  75. def OAI.MUB6.Certificate.MixedData.merged2117part23 line 177
  76. def OAI.MUB6.Certificate.MixedData.merged2117part24 line 179
  77. def OAI.MUB6.Certificate.MixedData.merged2117 line 181
  78. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2117 line 183
  79. theorem OAI.MUB6.Certificate.MixedData.mergedZero2117 line 185
  80. def OAI.MUB6.Certificate.MixedData.merged2118 line 191
  81. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2118 line 193
  82. theorem OAI.MUB6.Certificate.MixedData.mergedZero2118 line 195
  83. def OAI.MUB6.Certificate.MixedData.merged2119 line 200
  84. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2119 line 202
  85. theorem OAI.MUB6.Certificate.MixedData.mergedZero2119 line 204
  86. def OAI.MUB6.Certificate.MixedData.merged2120 line 209
  87. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2120 line 211
  88. theorem OAI.MUB6.Certificate.MixedData.mergedZero2120 line 213
  89. def OAI.MUB6.Certificate.MixedData.merged2121 line 219
  90. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2121 line 221
  91. theorem OAI.MUB6.Certificate.MixedData.mergedZero2121 line 223
  92. def OAI.MUB6.Certificate.MixedData.merged2122 line 228
  93. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2122 line 230
  94. theorem OAI.MUB6.Certificate.MixedData.mergedZero2122 line 232
  95. def OAI.MUB6.Certificate.MixedData.merged2123 line 237
  96. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2123 line 239
  97. theorem OAI.MUB6.Certificate.MixedData.mergedZero2123 line 241
  98. def OAI.MUB6.Certificate.MixedData.merged2124 line 247
  99. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2124 line 249
  100. theorem OAI.MUB6.Certificate.MixedData.mergedZero2124 line 251
  101. def OAI.MUB6.Certificate.MixedData.merged2125 line 257
  102. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2125 line 259
  103. theorem OAI.MUB6.Certificate.MixedData.mergedZero2125 line 261
  104. def OAI.MUB6.Certificate.MixedData.merged2126 line 267
  105. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2126 line 269
  106. theorem OAI.MUB6.Certificate.MixedData.mergedZero2126 line 271
  107. def OAI.MUB6.Certificate.MixedData.merged2127 line 276
  108. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2127 line 278
  109. theorem OAI.MUB6.Certificate.MixedData.mergedZero2127 line 280
  110. def OAI.MUB6.Certificate.MixedData.merged2128 line 285
  111. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2128 line 287
  112. theorem OAI.MUB6.Certificate.MixedData.mergedZero2128 line 289
  113. def OAI.MUB6.Certificate.MixedData.merged2129 line 295
  114. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2129 line 297
  115. theorem OAI.MUB6.Certificate.MixedData.mergedZero2129 line 299
  116. def OAI.MUB6.Certificate.MixedData.merged2130 line 305
  117. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2130 line 307
  118. theorem OAI.MUB6.Certificate.MixedData.mergedZero2130 line 309
  119. def OAI.MUB6.Certificate.MixedData.merged2131 line 314
  120. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2131 line 316
  121. theorem OAI.MUB6.Certificate.MixedData.mergedZero2131 line 318
  122. def OAI.MUB6.Certificate.MixedData.merged2132 line 323
  123. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2132 line 325
  124. theorem OAI.MUB6.Certificate.MixedData.mergedZero2132 line 327
  125. def OAI.MUB6.Certificate.MixedData.merged2133 line 333
  126. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2133 line 335
  127. theorem OAI.MUB6.Certificate.MixedData.mergedZero2133 line 337
  128. def OAI.MUB6.Certificate.MixedData.merged2134 line 343
  129. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2134 line 345
  130. theorem OAI.MUB6.Certificate.MixedData.mergedZero2134 line 347
  131. def OAI.MUB6.Certificate.MixedData.merged2135 line 353
  132. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2135 line 355
  133. theorem OAI.MUB6.Certificate.MixedData.mergedZero2135 line 357
  134. def OAI.MUB6.Certificate.MixedData.merged2136 line 363
  135. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2136 line 365
  136. theorem OAI.MUB6.Certificate.MixedData.mergedZero2136 line 367
  137. def OAI.MUB6.Certificate.MixedData.merged2137 line 372
  138. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2137 line 374
  139. theorem OAI.MUB6.Certificate.MixedData.mergedZero2137 line 376
  140. def OAI.MUB6.Certificate.MixedData.merged2138 line 381
  141. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2138 line 383
  142. theorem OAI.MUB6.Certificate.MixedData.mergedZero2138 line 385
  143. def OAI.MUB6.Certificate.MixedData.merged2139 line 391
  144. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2139 line 393
  145. theorem OAI.MUB6.Certificate.MixedData.mergedZero2139 line 395
  146. def OAI.MUB6.Certificate.MixedData.merged2140 line 400
  147. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2140 line 402
  148. theorem OAI.MUB6.Certificate.MixedData.mergedZero2140 line 404
  149. def OAI.MUB6.Certificate.MixedData.merged2141 line 409
  150. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2141 line 411
  151. theorem OAI.MUB6.Certificate.MixedData.mergedZero2141 line 413
  152. def OAI.MUB6.Certificate.MixedData.merged2142 line 419
  153. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2142 line 421
  154. theorem OAI.MUB6.Certificate.MixedData.mergedZero2142 line 423
  155. def OAI.MUB6.Certificate.MixedData.merged2143 line 429
  156. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2143 line 431
  157. theorem OAI.MUB6.Certificate.MixedData.mergedZero2143 line 433