OAI/Analysis/MutuallyUnbiased/MixedMerge/Block61.lean

GitHub source file

137 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1952 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1952 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1952 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1953 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1953 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1953 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged1954 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1954 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1954 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged1955 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1955 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1955 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged1956 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1956 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1956 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged1957 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1957 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1957 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged1958 line 66
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1958 line 68
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1958 line 70
  22. def OAI.MUB6.Certificate.MixedData.merged1959 line 75
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1959 line 77
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1959 line 79
  25. def OAI.MUB6.Certificate.MixedData.merged1960 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1960 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1960 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged1961 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1961 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1961 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged1962 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1962 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1962 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged1963part0 line 115
  35. def OAI.MUB6.Certificate.MixedData.merged1963part1 line 117
  36. def OAI.MUB6.Certificate.MixedData.merged1963part2 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged1963part3 line 121
  38. def OAI.MUB6.Certificate.MixedData.merged1963part4 line 123
  39. def OAI.MUB6.Certificate.MixedData.merged1963part5 line 125
  40. def OAI.MUB6.Certificate.MixedData.merged1963part6 line 127
  41. def OAI.MUB6.Certificate.MixedData.merged1963part7 line 129
  42. def OAI.MUB6.Certificate.MixedData.merged1963part8 line 131
  43. def OAI.MUB6.Certificate.MixedData.merged1963 line 133
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1963 line 135
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1963 line 137
  46. def OAI.MUB6.Certificate.MixedData.merged1964part0 line 143
  47. def OAI.MUB6.Certificate.MixedData.merged1964part1 line 145
  48. def OAI.MUB6.Certificate.MixedData.merged1964part2 line 147
  49. def OAI.MUB6.Certificate.MixedData.merged1964part3 line 149
  50. def OAI.MUB6.Certificate.MixedData.merged1964part4 line 151
  51. def OAI.MUB6.Certificate.MixedData.merged1964part5 line 153
  52. def OAI.MUB6.Certificate.MixedData.merged1964part6 line 155
  53. def OAI.MUB6.Certificate.MixedData.merged1964part7 line 157
  54. def OAI.MUB6.Certificate.MixedData.merged1964part8 line 159
  55. def OAI.MUB6.Certificate.MixedData.merged1964part9 line 161
  56. def OAI.MUB6.Certificate.MixedData.merged1964part10 line 163
  57. def OAI.MUB6.Certificate.MixedData.merged1964part11 line 165
  58. def OAI.MUB6.Certificate.MixedData.merged1964part12 line 167
  59. def OAI.MUB6.Certificate.MixedData.merged1964 line 169
  60. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1964 line 171
  61. theorem OAI.MUB6.Certificate.MixedData.mergedZero1964 line 173
  62. def OAI.MUB6.Certificate.MixedData.merged1965part0 line 179
  63. def OAI.MUB6.Certificate.MixedData.merged1965part1 line 181
  64. def OAI.MUB6.Certificate.MixedData.merged1965part2 line 183
  65. def OAI.MUB6.Certificate.MixedData.merged1965part3 line 185
  66. def OAI.MUB6.Certificate.MixedData.merged1965part4 line 187
  67. def OAI.MUB6.Certificate.MixedData.merged1965part5 line 189
  68. def OAI.MUB6.Certificate.MixedData.merged1965part6 line 191
  69. def OAI.MUB6.Certificate.MixedData.merged1965part7 line 193
  70. def OAI.MUB6.Certificate.MixedData.merged1965part8 line 195
  71. def OAI.MUB6.Certificate.MixedData.merged1965part9 line 197
  72. def OAI.MUB6.Certificate.MixedData.merged1965part10 line 199
  73. def OAI.MUB6.Certificate.MixedData.merged1965part11 line 201
  74. def OAI.MUB6.Certificate.MixedData.merged1965part12 line 203
  75. def OAI.MUB6.Certificate.MixedData.merged1965part13 line 205
  76. def OAI.MUB6.Certificate.MixedData.merged1965part14 line 207
  77. def OAI.MUB6.Certificate.MixedData.merged1965part15 line 209
  78. def OAI.MUB6.Certificate.MixedData.merged1965part16 line 211
  79. def OAI.MUB6.Certificate.MixedData.merged1965part17 line 213
  80. def OAI.MUB6.Certificate.MixedData.merged1965part18 line 215
  81. def OAI.MUB6.Certificate.MixedData.merged1965 line 217
  82. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1965 line 219
  83. theorem OAI.MUB6.Certificate.MixedData.mergedZero1965 line 221
  84. def OAI.MUB6.Certificate.MixedData.merged1966 line 227
  85. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1966 line 229
  86. theorem OAI.MUB6.Certificate.MixedData.mergedZero1966 line 231
  87. def OAI.MUB6.Certificate.MixedData.merged1967 line 236
  88. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1967 line 238
  89. theorem OAI.MUB6.Certificate.MixedData.mergedZero1967 line 240
  90. def OAI.MUB6.Certificate.MixedData.merged1968 line 245
  91. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1968 line 247
  92. theorem OAI.MUB6.Certificate.MixedData.mergedZero1968 line 249
  93. def OAI.MUB6.Certificate.MixedData.merged1969 line 255
  94. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1969 line 257
  95. theorem OAI.MUB6.Certificate.MixedData.mergedZero1969 line 259
  96. def OAI.MUB6.Certificate.MixedData.merged1970 line 264
  97. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1970 line 266
  98. theorem OAI.MUB6.Certificate.MixedData.mergedZero1970 line 268
  99. def OAI.MUB6.Certificate.MixedData.merged1971 line 273
  100. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1971 line 275
  101. theorem OAI.MUB6.Certificate.MixedData.mergedZero1971 line 277
  102. def OAI.MUB6.Certificate.MixedData.merged1972 line 283
  103. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1972 line 285
  104. theorem OAI.MUB6.Certificate.MixedData.mergedZero1972 line 287
  105. def OAI.MUB6.Certificate.MixedData.merged1973 line 293
  106. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1973 line 295
  107. theorem OAI.MUB6.Certificate.MixedData.mergedZero1973 line 297
  108. def OAI.MUB6.Certificate.MixedData.merged1974 line 303
  109. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1974 line 305
  110. theorem OAI.MUB6.Certificate.MixedData.mergedZero1974 line 307
  111. def OAI.MUB6.Certificate.MixedData.merged1975 line 312
  112. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1975 line 314
  113. theorem OAI.MUB6.Certificate.MixedData.mergedZero1975 line 316
  114. def OAI.MUB6.Certificate.MixedData.merged1976 line 321
  115. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1976 line 323
  116. theorem OAI.MUB6.Certificate.MixedData.mergedZero1976 line 325
  117. def OAI.MUB6.Certificate.MixedData.merged1977 line 331
  118. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1977 line 333
  119. theorem OAI.MUB6.Certificate.MixedData.mergedZero1977 line 335
  120. def OAI.MUB6.Certificate.MixedData.merged1978 line 341
  121. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1978 line 343
  122. theorem OAI.MUB6.Certificate.MixedData.mergedZero1978 line 345
  123. def OAI.MUB6.Certificate.MixedData.merged1979 line 350
  124. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1979 line 352
  125. theorem OAI.MUB6.Certificate.MixedData.mergedZero1979 line 354
  126. def OAI.MUB6.Certificate.MixedData.merged1980 line 359
  127. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1980 line 361
  128. theorem OAI.MUB6.Certificate.MixedData.mergedZero1980 line 363
  129. def OAI.MUB6.Certificate.MixedData.merged1981 line 369
  130. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1981 line 371
  131. theorem OAI.MUB6.Certificate.MixedData.mergedZero1981 line 373
  132. def OAI.MUB6.Certificate.MixedData.merged1982 line 379
  133. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1982 line 381
  134. theorem OAI.MUB6.Certificate.MixedData.mergedZero1982 line 383
  135. def OAI.MUB6.Certificate.MixedData.merged1983 line 389
  136. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1983 line 391
  137. theorem OAI.MUB6.Certificate.MixedData.mergedZero1983 line 393