OAI/Analysis/MutuallyUnbiased/MixedMerge/Block68.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged2176 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2176 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero2176 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged2177 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2177 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero2177 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged2178 line 27
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2178 line 29
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero2178 line 31
  10. def OAI.MUB6.Certificate.MixedData.merged2179 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2179 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero2179 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged2180 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2180 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero2180 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged2181 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2181 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero2181 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged2182 line 66
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2182 line 68
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero2182 line 70
  22. def OAI.MUB6.Certificate.MixedData.merged2183 line 75
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2183 line 77
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero2183 line 79
  25. def OAI.MUB6.Certificate.MixedData.merged2184 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2184 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero2184 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged2185 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2185 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero2185 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged2186 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2186 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero2186 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged2187 line 113
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2187 line 115
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero2187 line 117
  37. def OAI.MUB6.Certificate.MixedData.merged2188 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2188 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero2188 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged2189 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2189 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero2189 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged2190 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2190 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero2190 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged2191 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2191 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero2191 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged2192 line 163
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2192 line 165
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero2192 line 167
  52. def OAI.MUB6.Certificate.MixedData.merged2193 line 173
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2193 line 175
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero2193 line 177
  55. def OAI.MUB6.Certificate.MixedData.merged2194 line 182
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2194 line 184
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero2194 line 186
  58. def OAI.MUB6.Certificate.MixedData.merged2195 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2195 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero2195 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged2196 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2196 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero2196 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged2197 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2197 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero2197 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged2198 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2198 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero2198 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged2199 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2199 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero2199 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged2200 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2200 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero2200 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged2201 line 249
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2201 line 251
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero2201 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged2202 line 258
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2202 line 260
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero2202 line 262
  82. def OAI.MUB6.Certificate.MixedData.merged2203 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2203 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero2203 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged2204 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2204 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero2204 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged2205 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2205 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero2205 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged2206 line 296
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2206 line 298
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero2206 line 300
  94. def OAI.MUB6.Certificate.MixedData.merged2207 line 305
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2207 line 307
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero2207 line 309