OAI/Analysis/MutuallyUnbiased/MixedMerge/Block35.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1120 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1120 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1120 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1121 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1121 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1121 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged1122 line 27
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1122 line 29
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1122 line 31
  10. def OAI.MUB6.Certificate.MixedData.merged1123 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1123 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1123 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged1124 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1124 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1124 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged1125 line 56
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1125 line 58
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1125 line 60
  19. def OAI.MUB6.Certificate.MixedData.merged1126 line 65
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1126 line 67
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1126 line 69
  22. def OAI.MUB6.Certificate.MixedData.merged1127 line 75
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1127 line 77
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1127 line 79
  25. def OAI.MUB6.Certificate.MixedData.merged1128 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1128 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1128 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged1129 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1129 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1129 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged1130 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1130 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1130 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged1131 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1131 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1131 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged1132 line 125
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1132 line 127
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1132 line 129
  40. def OAI.MUB6.Certificate.MixedData.merged1133 line 134
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1133 line 136
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1133 line 138
  43. def OAI.MUB6.Certificate.MixedData.merged1134 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1134 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1134 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged1135 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1135 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1135 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged1136 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1136 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1136 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged1137 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1137 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1137 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged1138 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1138 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1138 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged1139 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1139 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1139 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged1140 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1140 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1140 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged1141 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1141 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1141 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged1142 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1142 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1142 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged1143 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1143 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1143 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged1144 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1144 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1144 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged1145 line 248
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1145 line 250
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1145 line 252
  79. def OAI.MUB6.Certificate.MixedData.merged1146 line 257
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1146 line 259
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1146 line 261
  82. def OAI.MUB6.Certificate.MixedData.merged1147 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1147 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero1147 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged1148 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1148 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero1148 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged1149 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1149 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero1149 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged1150 line 297
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1150 line 299
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero1150 line 301
  94. def OAI.MUB6.Certificate.MixedData.merged1151 line 306
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1151 line 308
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero1151 line 310