OAI/Analysis/MutuallyUnbiased/MixedMerge/Block60.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1920 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1920 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1920 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1921 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1921 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1921 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged1922 line 27
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1922 line 29
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1922 line 31
  10. def OAI.MUB6.Certificate.MixedData.merged1923 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1923 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1923 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged1924 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1924 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1924 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged1925 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1925 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1925 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged1926 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1926 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1926 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged1927 line 77
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1927 line 79
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1927 line 81
  25. def OAI.MUB6.Certificate.MixedData.merged1928 line 86
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1928 line 88
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1928 line 90
  28. def OAI.MUB6.Certificate.MixedData.merged1929 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1929 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1929 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged1930 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1930 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1930 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged1931 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1931 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1931 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged1932 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1932 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1932 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged1933 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1933 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1933 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged1934 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1934 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1934 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged1935 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1935 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1935 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged1936 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1936 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1936 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged1937 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1937 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1937 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged1938 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1938 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1938 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged1939 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1939 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1939 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged1940 line 200
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1940 line 202
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1940 line 204
  64. def OAI.MUB6.Certificate.MixedData.merged1941 line 209
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1941 line 211
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1941 line 213
  67. def OAI.MUB6.Certificate.MixedData.merged1942 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1942 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1942 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged1943 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1943 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1943 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged1944 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1944 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1944 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged1945 line 249
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1945 line 251
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1945 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged1946 line 258
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1946 line 260
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1946 line 262
  82. def OAI.MUB6.Certificate.MixedData.merged1947 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1947 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero1947 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged1948 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1948 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero1948 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged1949 line 286
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1949 line 288
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero1949 line 290
  91. def OAI.MUB6.Certificate.MixedData.merged1950 line 295
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1950 line 297
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero1950 line 299
  94. def OAI.MUB6.Certificate.MixedData.merged1951 line 305
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1951 line 307
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero1951 line 309