OAI/Analysis/MutuallyUnbiased/MixedMerge/Block6.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged192 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck192 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero192 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged193 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck193 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero193 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged194 line 29
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck194 line 31
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero194 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged195 line 39
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck195 line 41
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero195 line 43
  13. def OAI.MUB6.Certificate.MixedData.merged196 line 48
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck196 line 50
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero196 line 52
  16. def OAI.MUB6.Certificate.MixedData.merged197 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck197 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero197 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged198 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck198 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero198 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged199 line 77
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck199 line 79
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero199 line 81
  25. def OAI.MUB6.Certificate.MixedData.merged200 line 86
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck200 line 88
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero200 line 90
  28. def OAI.MUB6.Certificate.MixedData.merged201 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck201 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero201 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged202 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck202 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero202 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged203 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck203 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero203 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged204 line 125
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck204 line 127
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero204 line 129
  40. def OAI.MUB6.Certificate.MixedData.merged205 line 135
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck205 line 137
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero205 line 139
  43. def OAI.MUB6.Certificate.MixedData.merged206 line 144
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck206 line 146
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero206 line 148
  46. def OAI.MUB6.Certificate.MixedData.merged207 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck207 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero207 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged208 line 163
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck208 line 165
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero208 line 167
  52. def OAI.MUB6.Certificate.MixedData.merged209 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck209 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero209 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged210 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck210 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero210 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged211 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck211 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero211 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged212 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck212 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero212 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged213 line 211
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck213 line 213
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero213 line 215
  67. def OAI.MUB6.Certificate.MixedData.merged214 line 220
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck214 line 222
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero214 line 224
  70. def OAI.MUB6.Certificate.MixedData.merged215 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck215 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero215 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged216 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck216 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero216 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged217 line 249
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck217 line 251
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero217 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged218 line 258
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck218 line 260
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero218 line 262
  82. def OAI.MUB6.Certificate.MixedData.merged219 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck219 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero219 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged220 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck220 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero220 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged221 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck221 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero221 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged222 line 297
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck222 line 299
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero222 line 301
  94. def OAI.MUB6.Certificate.MixedData.merged223 line 307
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck223 line 309
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero223 line 311