OAI/Analysis/MutuallyUnbiased/MixedMerge/Block59.lean

GitHub source file

115 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1888part0 line 9
  2. def OAI.MUB6.Certificate.MixedData.merged1888part1 line 11
  3. def OAI.MUB6.Certificate.MixedData.merged1888part2 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1888part3 line 15
  5. def OAI.MUB6.Certificate.MixedData.merged1888part4 line 17
  6. def OAI.MUB6.Certificate.MixedData.merged1888part5 line 19
  7. def OAI.MUB6.Certificate.MixedData.merged1888part6 line 21
  8. def OAI.MUB6.Certificate.MixedData.merged1888 line 23
  9. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1888 line 25
  10. theorem OAI.MUB6.Certificate.MixedData.mergedZero1888 line 27
  11. def OAI.MUB6.Certificate.MixedData.merged1889part0 line 33
  12. def OAI.MUB6.Certificate.MixedData.merged1889part1 line 35
  13. def OAI.MUB6.Certificate.MixedData.merged1889part2 line 37
  14. def OAI.MUB6.Certificate.MixedData.merged1889part3 line 39
  15. def OAI.MUB6.Certificate.MixedData.merged1889part4 line 41
  16. def OAI.MUB6.Certificate.MixedData.merged1889part5 line 43
  17. def OAI.MUB6.Certificate.MixedData.merged1889part6 line 45
  18. def OAI.MUB6.Certificate.MixedData.merged1889part7 line 47
  19. def OAI.MUB6.Certificate.MixedData.merged1889part8 line 49
  20. def OAI.MUB6.Certificate.MixedData.merged1889part9 line 51
  21. def OAI.MUB6.Certificate.MixedData.merged1889part10 line 53
  22. def OAI.MUB6.Certificate.MixedData.merged1889part11 line 55
  23. def OAI.MUB6.Certificate.MixedData.merged1889 line 57
  24. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1889 line 59
  25. theorem OAI.MUB6.Certificate.MixedData.mergedZero1889 line 61
  26. def OAI.MUB6.Certificate.MixedData.merged1890 line 67
  27. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1890 line 69
  28. theorem OAI.MUB6.Certificate.MixedData.mergedZero1890 line 71
  29. def OAI.MUB6.Certificate.MixedData.merged1891 line 76
  30. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1891 line 78
  31. theorem OAI.MUB6.Certificate.MixedData.mergedZero1891 line 80
  32. def OAI.MUB6.Certificate.MixedData.merged1892 line 85
  33. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1892 line 87
  34. theorem OAI.MUB6.Certificate.MixedData.mergedZero1892 line 89
  35. def OAI.MUB6.Certificate.MixedData.merged1893 line 95
  36. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1893 line 97
  37. theorem OAI.MUB6.Certificate.MixedData.mergedZero1893 line 99
  38. def OAI.MUB6.Certificate.MixedData.merged1894 line 104
  39. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1894 line 106
  40. theorem OAI.MUB6.Certificate.MixedData.mergedZero1894 line 108
  41. def OAI.MUB6.Certificate.MixedData.merged1895 line 113
  42. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1895 line 115
  43. theorem OAI.MUB6.Certificate.MixedData.mergedZero1895 line 117
  44. def OAI.MUB6.Certificate.MixedData.merged1896 line 123
  45. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1896 line 125
  46. theorem OAI.MUB6.Certificate.MixedData.mergedZero1896 line 127
  47. def OAI.MUB6.Certificate.MixedData.merged1897 line 133
  48. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1897 line 135
  49. theorem OAI.MUB6.Certificate.MixedData.mergedZero1897 line 137
  50. def OAI.MUB6.Certificate.MixedData.merged1898 line 143
  51. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1898 line 145
  52. theorem OAI.MUB6.Certificate.MixedData.mergedZero1898 line 147
  53. def OAI.MUB6.Certificate.MixedData.merged1899 line 152
  54. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1899 line 154
  55. theorem OAI.MUB6.Certificate.MixedData.mergedZero1899 line 156
  56. def OAI.MUB6.Certificate.MixedData.merged1900 line 161
  57. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1900 line 163
  58. theorem OAI.MUB6.Certificate.MixedData.mergedZero1900 line 165
  59. def OAI.MUB6.Certificate.MixedData.merged1901 line 171
  60. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1901 line 173
  61. theorem OAI.MUB6.Certificate.MixedData.mergedZero1901 line 175
  62. def OAI.MUB6.Certificate.MixedData.merged1902 line 181
  63. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1902 line 183
  64. theorem OAI.MUB6.Certificate.MixedData.mergedZero1902 line 185
  65. def OAI.MUB6.Certificate.MixedData.merged1903 line 190
  66. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1903 line 192
  67. theorem OAI.MUB6.Certificate.MixedData.mergedZero1903 line 194
  68. def OAI.MUB6.Certificate.MixedData.merged1904 line 199
  69. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1904 line 201
  70. theorem OAI.MUB6.Certificate.MixedData.mergedZero1904 line 203
  71. def OAI.MUB6.Certificate.MixedData.merged1905 line 209
  72. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1905 line 211
  73. theorem OAI.MUB6.Certificate.MixedData.mergedZero1905 line 213
  74. def OAI.MUB6.Certificate.MixedData.merged1906 line 219
  75. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1906 line 221
  76. theorem OAI.MUB6.Certificate.MixedData.mergedZero1906 line 223
  77. def OAI.MUB6.Certificate.MixedData.merged1907 line 229
  78. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1907 line 231
  79. theorem OAI.MUB6.Certificate.MixedData.mergedZero1907 line 233
  80. def OAI.MUB6.Certificate.MixedData.merged1908 line 239
  81. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1908 line 241
  82. theorem OAI.MUB6.Certificate.MixedData.mergedZero1908 line 243
  83. def OAI.MUB6.Certificate.MixedData.merged1909 line 248
  84. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1909 line 250
  85. theorem OAI.MUB6.Certificate.MixedData.mergedZero1909 line 252
  86. def OAI.MUB6.Certificate.MixedData.merged1910 line 257
  87. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1910 line 259
  88. theorem OAI.MUB6.Certificate.MixedData.mergedZero1910 line 261
  89. def OAI.MUB6.Certificate.MixedData.merged1911 line 267
  90. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1911 line 269
  91. theorem OAI.MUB6.Certificate.MixedData.mergedZero1911 line 271
  92. def OAI.MUB6.Certificate.MixedData.merged1912 line 276
  93. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1912 line 278
  94. theorem OAI.MUB6.Certificate.MixedData.mergedZero1912 line 280
  95. def OAI.MUB6.Certificate.MixedData.merged1913 line 285
  96. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1913 line 287
  97. theorem OAI.MUB6.Certificate.MixedData.mergedZero1913 line 289
  98. def OAI.MUB6.Certificate.MixedData.merged1914 line 295
  99. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1914 line 297
  100. theorem OAI.MUB6.Certificate.MixedData.mergedZero1914 line 299
  101. def OAI.MUB6.Certificate.MixedData.merged1915 line 305
  102. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1915 line 307
  103. theorem OAI.MUB6.Certificate.MixedData.mergedZero1915 line 309
  104. def OAI.MUB6.Certificate.MixedData.merged1916 line 315
  105. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1916 line 317
  106. theorem OAI.MUB6.Certificate.MixedData.mergedZero1916 line 319
  107. def OAI.MUB6.Certificate.MixedData.merged1917 line 324
  108. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1917 line 326
  109. theorem OAI.MUB6.Certificate.MixedData.mergedZero1917 line 328
  110. def OAI.MUB6.Certificate.MixedData.merged1918 line 333
  111. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1918 line 335
  112. theorem OAI.MUB6.Certificate.MixedData.mergedZero1918 line 337
  113. def OAI.MUB6.Certificate.MixedData.merged1919 line 343
  114. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1919 line 345
  115. theorem OAI.MUB6.Certificate.MixedData.mergedZero1919 line 347