OAI/Analysis/MutuallyUnbiased/MixedMerge/Block9.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged288 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck288 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero288 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged289 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck289 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero289 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged290 line 27
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck290 line 29
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero290 line 31
  10. def OAI.MUB6.Certificate.MixedData.merged291 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck291 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero291 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged292 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck292 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero292 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged293 line 56
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck293 line 58
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero293 line 60
  19. def OAI.MUB6.Certificate.MixedData.merged294 line 65
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck294 line 67
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero294 line 69
  22. def OAI.MUB6.Certificate.MixedData.merged295 line 75
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck295 line 77
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero295 line 79
  25. def OAI.MUB6.Certificate.MixedData.merged296 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck296 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero296 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged297 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck297 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero297 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged298 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck298 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero298 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged299 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck299 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero299 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged300part0 line 125
  38. def OAI.MUB6.Certificate.MixedData.merged300part1 line 127
  39. def OAI.MUB6.Certificate.MixedData.merged300part2 line 129
  40. def OAI.MUB6.Certificate.MixedData.merged300part3 line 131
  41. def OAI.MUB6.Certificate.MixedData.merged300part4 line 133
  42. def OAI.MUB6.Certificate.MixedData.merged300part5 line 135
  43. def OAI.MUB6.Certificate.MixedData.merged300part6 line 137
  44. def OAI.MUB6.Certificate.MixedData.merged300part7 line 139
  45. def OAI.MUB6.Certificate.MixedData.merged300part8 line 141
  46. def OAI.MUB6.Certificate.MixedData.merged300 line 143
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck300 line 145
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero300 line 147
  49. def OAI.MUB6.Certificate.MixedData.merged301part0 line 153
  50. def OAI.MUB6.Certificate.MixedData.merged301part1 line 155
  51. def OAI.MUB6.Certificate.MixedData.merged301part2 line 157
  52. def OAI.MUB6.Certificate.MixedData.merged301part3 line 159
  53. def OAI.MUB6.Certificate.MixedData.merged301part4 line 161
  54. def OAI.MUB6.Certificate.MixedData.merged301part5 line 163
  55. def OAI.MUB6.Certificate.MixedData.merged301part6 line 165
  56. def OAI.MUB6.Certificate.MixedData.merged301part7 line 167
  57. def OAI.MUB6.Certificate.MixedData.merged301part8 line 169
  58. def OAI.MUB6.Certificate.MixedData.merged301part9 line 171
  59. def OAI.MUB6.Certificate.MixedData.merged301part10 line 173
  60. def OAI.MUB6.Certificate.MixedData.merged301part11 line 175
  61. def OAI.MUB6.Certificate.MixedData.merged301 line 177
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck301 line 179
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero301 line 181
  64. def OAI.MUB6.Certificate.MixedData.merged302 line 187
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck302 line 189
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero302 line 191
  67. def OAI.MUB6.Certificate.MixedData.merged303 line 196
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck303 line 198
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero303 line 200
  70. def OAI.MUB6.Certificate.MixedData.merged304 line 205
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck304 line 207
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero304 line 209
  73. def OAI.MUB6.Certificate.MixedData.merged305 line 215
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck305 line 217
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero305 line 219
  76. def OAI.MUB6.Certificate.MixedData.merged306 line 224
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck306 line 226
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero306 line 228
  79. def OAI.MUB6.Certificate.MixedData.merged307 line 233
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck307 line 235
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero307 line 237
  82. def OAI.MUB6.Certificate.MixedData.merged308 line 243
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck308 line 245
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero308 line 247
  85. def OAI.MUB6.Certificate.MixedData.merged309 line 253
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck309 line 255
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero309 line 257
  88. def OAI.MUB6.Certificate.MixedData.merged310 line 263
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck310 line 265
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero310 line 267
  91. def OAI.MUB6.Certificate.MixedData.merged311 line 272
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck311 line 274
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero311 line 276
  94. def OAI.MUB6.Certificate.MixedData.merged312 line 281
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck312 line 283
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero312 line 285
  97. def OAI.MUB6.Certificate.MixedData.merged313 line 291
  98. theorem OAI.MUB6.Certificate.MixedData.mergeCheck313 line 293
  99. theorem OAI.MUB6.Certificate.MixedData.mergedZero313 line 295
  100. def OAI.MUB6.Certificate.MixedData.merged314 line 300
  101. theorem OAI.MUB6.Certificate.MixedData.mergeCheck314 line 302
  102. theorem OAI.MUB6.Certificate.MixedData.mergedZero314 line 304
  103. def OAI.MUB6.Certificate.MixedData.merged315 line 309
  104. theorem OAI.MUB6.Certificate.MixedData.mergeCheck315 line 311
  105. theorem OAI.MUB6.Certificate.MixedData.mergedZero315 line 313
  106. def OAI.MUB6.Certificate.MixedData.merged316 line 319
  107. theorem OAI.MUB6.Certificate.MixedData.mergeCheck316 line 321
  108. theorem OAI.MUB6.Certificate.MixedData.mergedZero316 line 323
  109. def OAI.MUB6.Certificate.MixedData.merged317 line 329
  110. theorem OAI.MUB6.Certificate.MixedData.mergeCheck317 line 331
  111. theorem OAI.MUB6.Certificate.MixedData.mergedZero317 line 333
  112. def OAI.MUB6.Certificate.MixedData.merged318 line 339
  113. theorem OAI.MUB6.Certificate.MixedData.mergeCheck318 line 341
  114. theorem OAI.MUB6.Certificate.MixedData.mergedZero318 line 343
  115. def OAI.MUB6.Certificate.MixedData.merged319 line 349
  116. theorem OAI.MUB6.Certificate.MixedData.mergeCheck319 line 351
  117. theorem OAI.MUB6.Certificate.MixedData.mergedZero319 line 353