OAI/Analysis/MutuallyUnbiased/MixedMerge/Block4.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged128 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck128 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero128 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged129 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck129 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero129 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged130 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck130 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero130 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged131 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck131 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero131 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged132 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck132 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero132 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged133 line 56
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck133 line 58
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero133 line 60
  19. def OAI.MUB6.Certificate.MixedData.merged134 line 65
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck134 line 67
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero134 line 69
  22. def OAI.MUB6.Certificate.MixedData.merged135 line 75
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck135 line 77
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero135 line 79
  25. def OAI.MUB6.Certificate.MixedData.merged136 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck136 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero136 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged137 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck137 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero137 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged138 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck138 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero138 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged139 line 113
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck139 line 115
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero139 line 117
  37. def OAI.MUB6.Certificate.MixedData.merged140 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck140 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero140 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged141 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck141 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero141 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged142 line 142
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck142 line 144
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero142 line 146
  46. def OAI.MUB6.Certificate.MixedData.merged143 line 151
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck143 line 153
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero143 line 155
  49. def OAI.MUB6.Certificate.MixedData.merged144 line 161
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck144 line 163
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero144 line 165
  52. def OAI.MUB6.Certificate.MixedData.merged145 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck145 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero145 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged146 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck146 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero146 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged147 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck147 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero147 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged148 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck148 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero148 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged149 line 211
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck149 line 213
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero149 line 215
  67. def OAI.MUB6.Certificate.MixedData.merged150 line 221
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck150 line 223
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero150 line 225
  70. def OAI.MUB6.Certificate.MixedData.merged151 line 230
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck151 line 232
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero151 line 234
  73. def OAI.MUB6.Certificate.MixedData.merged152 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck152 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero152 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged153 line 249
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck153 line 251
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero153 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged154 line 258
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck154 line 260
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero154 line 262
  82. def OAI.MUB6.Certificate.MixedData.merged155 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck155 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero155 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged156 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck156 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero156 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged157 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck157 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero157 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged158 line 297
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck158 line 299
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero158 line 301
  94. def OAI.MUB6.Certificate.MixedData.merged159 line 306
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck159 line 308
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero159 line 310