OAI/Analysis/MutuallyUnbiased/MixedMerge/Block63.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged2016 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2016 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero2016 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged2017 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2017 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero2017 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged2018 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2018 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero2018 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged2019 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2019 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero2019 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged2020 line 48
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2020 line 50
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero2020 line 52
  16. def OAI.MUB6.Certificate.MixedData.merged2021 line 58
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2021 line 60
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero2021 line 62
  19. def OAI.MUB6.Certificate.MixedData.merged2022 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2022 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero2022 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged2023 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2023 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero2023 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged2024 line 86
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2024 line 88
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero2024 line 90
  28. def OAI.MUB6.Certificate.MixedData.merged2025 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2025 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero2025 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged2026 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2026 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero2026 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged2027 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2027 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero2027 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged2028 line 124
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2028 line 126
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero2028 line 128
  40. def OAI.MUB6.Certificate.MixedData.merged2029 line 134
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2029 line 136
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero2029 line 138
  43. def OAI.MUB6.Certificate.MixedData.merged2030 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2030 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero2030 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged2031 line 152
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2031 line 154
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero2031 line 156
  49. def OAI.MUB6.Certificate.MixedData.merged2032 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2032 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero2032 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged2033 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2033 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero2033 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged2034 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2034 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero2034 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged2035 line 190
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2035 line 192
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero2035 line 194
  61. def OAI.MUB6.Certificate.MixedData.merged2036 line 200
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2036 line 202
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero2036 line 204
  64. def OAI.MUB6.Certificate.MixedData.merged2037 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2037 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero2037 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged2038 line 220
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2038 line 222
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero2038 line 224
  70. def OAI.MUB6.Certificate.MixedData.merged2039part0 line 230
  71. def OAI.MUB6.Certificate.MixedData.merged2039part1 line 232
  72. def OAI.MUB6.Certificate.MixedData.merged2039part2 line 234
  73. def OAI.MUB6.Certificate.MixedData.merged2039part3 line 236
  74. def OAI.MUB6.Certificate.MixedData.merged2039part4 line 238
  75. def OAI.MUB6.Certificate.MixedData.merged2039part5 line 240
  76. def OAI.MUB6.Certificate.MixedData.merged2039part6 line 242
  77. def OAI.MUB6.Certificate.MixedData.merged2039 line 244
  78. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2039 line 246
  79. theorem OAI.MUB6.Certificate.MixedData.mergedZero2039 line 248
  80. def OAI.MUB6.Certificate.MixedData.merged2040part0 line 254
  81. def OAI.MUB6.Certificate.MixedData.merged2040part1 line 256
  82. def OAI.MUB6.Certificate.MixedData.merged2040part2 line 258
  83. def OAI.MUB6.Certificate.MixedData.merged2040part3 line 260
  84. def OAI.MUB6.Certificate.MixedData.merged2040part4 line 262
  85. def OAI.MUB6.Certificate.MixedData.merged2040part5 line 264
  86. def OAI.MUB6.Certificate.MixedData.merged2040part6 line 266
  87. def OAI.MUB6.Certificate.MixedData.merged2040part7 line 268
  88. def OAI.MUB6.Certificate.MixedData.merged2040part8 line 270
  89. def OAI.MUB6.Certificate.MixedData.merged2040part9 line 272
  90. def OAI.MUB6.Certificate.MixedData.merged2040part10 line 274
  91. def OAI.MUB6.Certificate.MixedData.merged2040part11 line 276
  92. def OAI.MUB6.Certificate.MixedData.merged2040part12 line 278
  93. def OAI.MUB6.Certificate.MixedData.merged2040 line 280
  94. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2040 line 282
  95. theorem OAI.MUB6.Certificate.MixedData.mergedZero2040 line 284
  96. def OAI.MUB6.Certificate.MixedData.merged2041 line 290
  97. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2041 line 292
  98. theorem OAI.MUB6.Certificate.MixedData.mergedZero2041 line 294
  99. def OAI.MUB6.Certificate.MixedData.merged2042 line 299
  100. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2042 line 301
  101. theorem OAI.MUB6.Certificate.MixedData.mergedZero2042 line 303
  102. def OAI.MUB6.Certificate.MixedData.merged2043 line 308
  103. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2043 line 310
  104. theorem OAI.MUB6.Certificate.MixedData.mergedZero2043 line 312
  105. def OAI.MUB6.Certificate.MixedData.merged2044 line 318
  106. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2044 line 320
  107. theorem OAI.MUB6.Certificate.MixedData.mergedZero2044 line 322
  108. def OAI.MUB6.Certificate.MixedData.merged2045 line 327
  109. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2045 line 329
  110. theorem OAI.MUB6.Certificate.MixedData.mergedZero2045 line 331
  111. def OAI.MUB6.Certificate.MixedData.merged2046 line 336
  112. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2046 line 338
  113. theorem OAI.MUB6.Certificate.MixedData.mergedZero2046 line 340
  114. def OAI.MUB6.Certificate.MixedData.merged2047 line 346
  115. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2047 line 348
  116. theorem OAI.MUB6.Certificate.MixedData.mergedZero2047 line 350