OAI/Analysis/MutuallyUnbiased/MixedMerge/Block28.lean

GitHub source file

135 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged896 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck896 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero896 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged897 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck897 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero897 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged898 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck898 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero898 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged899 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck899 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero899 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged900 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck900 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero900 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged901 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck901 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero901 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged902 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck902 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero902 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged903 line 77
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck903 line 79
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero903 line 81
  25. def OAI.MUB6.Certificate.MixedData.merged904part0 line 87
  26. def OAI.MUB6.Certificate.MixedData.merged904part1 line 89
  27. def OAI.MUB6.Certificate.MixedData.merged904part2 line 91
  28. def OAI.MUB6.Certificate.MixedData.merged904part3 line 93
  29. def OAI.MUB6.Certificate.MixedData.merged904part4 line 95
  30. def OAI.MUB6.Certificate.MixedData.merged904part5 line 97
  31. def OAI.MUB6.Certificate.MixedData.merged904part6 line 99
  32. def OAI.MUB6.Certificate.MixedData.merged904part7 line 101
  33. def OAI.MUB6.Certificate.MixedData.merged904part8 line 103
  34. def OAI.MUB6.Certificate.MixedData.merged904 line 105
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck904 line 107
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero904 line 109
  37. def OAI.MUB6.Certificate.MixedData.merged905part0 line 115
  38. def OAI.MUB6.Certificate.MixedData.merged905part1 line 117
  39. def OAI.MUB6.Certificate.MixedData.merged905part2 line 119
  40. def OAI.MUB6.Certificate.MixedData.merged905part3 line 121
  41. def OAI.MUB6.Certificate.MixedData.merged905part4 line 123
  42. def OAI.MUB6.Certificate.MixedData.merged905part5 line 125
  43. def OAI.MUB6.Certificate.MixedData.merged905part6 line 127
  44. def OAI.MUB6.Certificate.MixedData.merged905part7 line 129
  45. def OAI.MUB6.Certificate.MixedData.merged905part8 line 131
  46. def OAI.MUB6.Certificate.MixedData.merged905part9 line 133
  47. def OAI.MUB6.Certificate.MixedData.merged905part10 line 135
  48. def OAI.MUB6.Certificate.MixedData.merged905part11 line 137
  49. def OAI.MUB6.Certificate.MixedData.merged905 line 139
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck905 line 141
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero905 line 143
  52. def OAI.MUB6.Certificate.MixedData.merged906part0 line 149
  53. def OAI.MUB6.Certificate.MixedData.merged906part1 line 151
  54. def OAI.MUB6.Certificate.MixedData.merged906part2 line 153
  55. def OAI.MUB6.Certificate.MixedData.merged906part3 line 155
  56. def OAI.MUB6.Certificate.MixedData.merged906part4 line 157
  57. def OAI.MUB6.Certificate.MixedData.merged906part5 line 159
  58. def OAI.MUB6.Certificate.MixedData.merged906part6 line 161
  59. def OAI.MUB6.Certificate.MixedData.merged906part7 line 163
  60. def OAI.MUB6.Certificate.MixedData.merged906part8 line 165
  61. def OAI.MUB6.Certificate.MixedData.merged906part9 line 167
  62. def OAI.MUB6.Certificate.MixedData.merged906part10 line 169
  63. def OAI.MUB6.Certificate.MixedData.merged906part11 line 171
  64. def OAI.MUB6.Certificate.MixedData.merged906part12 line 173
  65. def OAI.MUB6.Certificate.MixedData.merged906part13 line 175
  66. def OAI.MUB6.Certificate.MixedData.merged906part14 line 177
  67. def OAI.MUB6.Certificate.MixedData.merged906part15 line 179
  68. def OAI.MUB6.Certificate.MixedData.merged906part16 line 181
  69. def OAI.MUB6.Certificate.MixedData.merged906part17 line 183
  70. def OAI.MUB6.Certificate.MixedData.merged906 line 185
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck906 line 187
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero906 line 189
  73. def OAI.MUB6.Certificate.MixedData.merged907 line 195
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck907 line 197
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero907 line 199
  76. def OAI.MUB6.Certificate.MixedData.merged908 line 204
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck908 line 206
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero908 line 208
  79. def OAI.MUB6.Certificate.MixedData.merged909 line 213
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck909 line 215
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero909 line 217
  82. def OAI.MUB6.Certificate.MixedData.merged910 line 223
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck910 line 225
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero910 line 227
  85. def OAI.MUB6.Certificate.MixedData.merged911 line 232
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck911 line 234
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero911 line 236
  88. def OAI.MUB6.Certificate.MixedData.merged912 line 241
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck912 line 243
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero912 line 245
  91. def OAI.MUB6.Certificate.MixedData.merged913 line 251
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck913 line 253
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero913 line 255
  94. def OAI.MUB6.Certificate.MixedData.merged914 line 261
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck914 line 263
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero914 line 265
  97. def OAI.MUB6.Certificate.MixedData.merged915 line 271
  98. theorem OAI.MUB6.Certificate.MixedData.mergeCheck915 line 273
  99. theorem OAI.MUB6.Certificate.MixedData.mergedZero915 line 275
  100. def OAI.MUB6.Certificate.MixedData.merged916 line 280
  101. theorem OAI.MUB6.Certificate.MixedData.mergeCheck916 line 282
  102. theorem OAI.MUB6.Certificate.MixedData.mergedZero916 line 284
  103. def OAI.MUB6.Certificate.MixedData.merged917 line 289
  104. theorem OAI.MUB6.Certificate.MixedData.mergeCheck917 line 291
  105. theorem OAI.MUB6.Certificate.MixedData.mergedZero917 line 293
  106. def OAI.MUB6.Certificate.MixedData.merged918 line 299
  107. theorem OAI.MUB6.Certificate.MixedData.mergeCheck918 line 301
  108. theorem OAI.MUB6.Certificate.MixedData.mergedZero918 line 303
  109. def OAI.MUB6.Certificate.MixedData.merged919 line 308
  110. theorem OAI.MUB6.Certificate.MixedData.mergeCheck919 line 310
  111. theorem OAI.MUB6.Certificate.MixedData.mergedZero919 line 312
  112. def OAI.MUB6.Certificate.MixedData.merged920 line 317
  113. theorem OAI.MUB6.Certificate.MixedData.mergeCheck920 line 319
  114. theorem OAI.MUB6.Certificate.MixedData.mergedZero920 line 321
  115. def OAI.MUB6.Certificate.MixedData.merged921 line 327
  116. theorem OAI.MUB6.Certificate.MixedData.mergeCheck921 line 329
  117. theorem OAI.MUB6.Certificate.MixedData.mergedZero921 line 331
  118. def OAI.MUB6.Certificate.MixedData.merged922 line 337
  119. theorem OAI.MUB6.Certificate.MixedData.mergeCheck922 line 339
  120. theorem OAI.MUB6.Certificate.MixedData.mergedZero922 line 341
  121. def OAI.MUB6.Certificate.MixedData.merged923 line 347
  122. theorem OAI.MUB6.Certificate.MixedData.mergeCheck923 line 349
  123. theorem OAI.MUB6.Certificate.MixedData.mergedZero923 line 351
  124. def OAI.MUB6.Certificate.MixedData.merged924 line 357
  125. theorem OAI.MUB6.Certificate.MixedData.mergeCheck924 line 359
  126. theorem OAI.MUB6.Certificate.MixedData.mergedZero924 line 361
  127. def OAI.MUB6.Certificate.MixedData.merged925 line 366
  128. theorem OAI.MUB6.Certificate.MixedData.mergeCheck925 line 368
  129. theorem OAI.MUB6.Certificate.MixedData.mergedZero925 line 370
  130. def OAI.MUB6.Certificate.MixedData.merged926 line 375
  131. theorem OAI.MUB6.Certificate.MixedData.mergeCheck926 line 377
  132. theorem OAI.MUB6.Certificate.MixedData.mergedZero926 line 379
  133. def OAI.MUB6.Certificate.MixedData.merged927 line 385
  134. theorem OAI.MUB6.Certificate.MixedData.mergeCheck927 line 387
  135. theorem OAI.MUB6.Certificate.MixedData.mergedZero927 line 389