OAI/Analysis/MutuallyUnbiased/MixedMerge/Block67.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged2144 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2144 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero2144 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged2145 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2145 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero2145 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged2146 line 27
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2146 line 29
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero2146 line 31
  10. def OAI.MUB6.Certificate.MixedData.merged2147 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2147 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero2147 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged2148 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2148 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero2148 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged2149 line 56
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2149 line 58
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero2149 line 60
  19. def OAI.MUB6.Certificate.MixedData.merged2150 line 65
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2150 line 67
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero2150 line 69
  22. def OAI.MUB6.Certificate.MixedData.merged2151 line 75
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2151 line 77
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero2151 line 79
  25. def OAI.MUB6.Certificate.MixedData.merged2152 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2152 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero2152 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged2153 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2153 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero2153 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged2154 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2154 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero2154 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged2155 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2155 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero2155 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged2156 line 124
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2156 line 126
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero2156 line 128
  40. def OAI.MUB6.Certificate.MixedData.merged2157 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2157 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero2157 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged2158 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2158 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero2158 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged2159 line 152
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2159 line 154
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero2159 line 156
  49. def OAI.MUB6.Certificate.MixedData.merged2160 line 161
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2160 line 163
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero2160 line 165
  52. def OAI.MUB6.Certificate.MixedData.merged2161 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2161 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero2161 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged2162 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2162 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero2162 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged2163 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2163 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero2163 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged2164 line 200
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2164 line 202
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero2164 line 204
  64. def OAI.MUB6.Certificate.MixedData.merged2165 line 209
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2165 line 211
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero2165 line 213
  67. def OAI.MUB6.Certificate.MixedData.merged2166 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2166 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero2166 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged2167 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2167 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero2167 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged2168 line 238
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2168 line 240
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero2168 line 242
  76. def OAI.MUB6.Certificate.MixedData.merged2169 line 247
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2169 line 249
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero2169 line 251
  79. def OAI.MUB6.Certificate.MixedData.merged2170 line 257
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2170 line 259
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero2170 line 261
  82. def OAI.MUB6.Certificate.MixedData.merged2171 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2171 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero2171 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged2172 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2172 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero2172 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged2173 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2173 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero2173 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged2174 line 296
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2174 line 298
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero2174 line 300
  94. def OAI.MUB6.Certificate.MixedData.merged2175 line 305
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2175 line 307
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero2175 line 309