OAI/Analysis/MutuallyUnbiased/MixedMerge/Block5.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged160 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck160 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero160 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged161 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck161 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero161 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged162 line 29
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck162 line 31
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero162 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged163 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck163 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero163 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged164 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck164 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero164 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged165 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck165 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero165 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged166 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck166 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero166 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged167 line 77
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck167 line 79
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero167 line 81
  25. def OAI.MUB6.Certificate.MixedData.merged168 line 87
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck168 line 89
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero168 line 91
  28. def OAI.MUB6.Certificate.MixedData.merged169 line 96
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck169 line 98
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero169 line 100
  31. def OAI.MUB6.Certificate.MixedData.merged170 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck170 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero170 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged171 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck171 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero171 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged172 line 124
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck172 line 126
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero172 line 128
  40. def OAI.MUB6.Certificate.MixedData.merged173 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck173 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero173 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged174 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck174 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero174 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged175 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck175 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero175 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged176 line 163
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck176 line 165
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero176 line 167
  52. def OAI.MUB6.Certificate.MixedData.merged177 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck177 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero177 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged178 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck178 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero178 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged179 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck179 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero179 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged180 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck180 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero180 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged181 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck181 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero181 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged182 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck182 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero182 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged183 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck183 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero183 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged184 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck184 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero184 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged185 line 249
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck185 line 251
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero185 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged186 line 259
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck186 line 261
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero186 line 263
  82. def OAI.MUB6.Certificate.MixedData.merged187 line 269
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck187 line 271
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero187 line 273
  85. def OAI.MUB6.Certificate.MixedData.merged188 line 278
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck188 line 280
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero188 line 282
  88. def OAI.MUB6.Certificate.MixedData.merged189 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck189 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero189 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged190 line 297
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck190 line 299
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero190 line 301
  94. def OAI.MUB6.Certificate.MixedData.merged191 line 306
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck191 line 308
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero191 line 310