OAI/Analysis/MutuallyUnbiased/MixedMerge/Block36.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1152 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1152 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1152 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1153 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1153 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1153 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged1154 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1154 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1154 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged1155 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1155 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1155 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged1156 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1156 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1156 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged1157 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1157 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1157 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged1158 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1158 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1158 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged1159 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1159 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1159 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged1160 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1160 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1160 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged1161 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1161 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1161 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged1162 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1162 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1162 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged1163 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1163 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1163 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged1164 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1164 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1164 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged1165 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1165 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1165 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged1166 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1166 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1166 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged1167 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1167 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1167 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged1168 line 163
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1168 line 165
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1168 line 167
  52. def OAI.MUB6.Certificate.MixedData.merged1169 line 173
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1169 line 175
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1169 line 177
  55. def OAI.MUB6.Certificate.MixedData.merged1170 line 182
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1170 line 184
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1170 line 186
  58. def OAI.MUB6.Certificate.MixedData.merged1171 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1171 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1171 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged1172 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1172 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1172 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged1173 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1173 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1173 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged1174 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1174 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1174 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged1175 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1175 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1175 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged1176 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1176 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1176 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged1177 line 249
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1177 line 251
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1177 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged1178 line 258
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1178 line 260
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1178 line 262
  82. def OAI.MUB6.Certificate.MixedData.merged1179 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1179 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero1179 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged1180 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1180 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero1180 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged1181 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1181 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero1181 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged1182 line 296
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1182 line 298
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero1182 line 300
  94. def OAI.MUB6.Certificate.MixedData.merged1183 line 305
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1183 line 307
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero1183 line 309