OAI/Analysis/MutuallyUnbiased/MixedMerge/Block23.lean

GitHub source file

116 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged736 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck736 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero736 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged737 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck737 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero737 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged738 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck738 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero738 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged739 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck739 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero739 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged740 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck740 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero740 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged741 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck741 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero741 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged742 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck742 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero742 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged743 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck743 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero743 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged744 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck744 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero744 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged745 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck745 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero745 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged746 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck746 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero746 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged747 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck747 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero747 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged748 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck748 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero748 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged749 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck749 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero749 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged750 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck750 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero750 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged751 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck751 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero751 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged752 line 163
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck752 line 165
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero752 line 167
  52. def OAI.MUB6.Certificate.MixedData.merged753part0 line 173
  53. def OAI.MUB6.Certificate.MixedData.merged753part1 line 175
  54. def OAI.MUB6.Certificate.MixedData.merged753part2 line 177
  55. def OAI.MUB6.Certificate.MixedData.merged753part3 line 179
  56. def OAI.MUB6.Certificate.MixedData.merged753part4 line 181
  57. def OAI.MUB6.Certificate.MixedData.merged753part5 line 183
  58. def OAI.MUB6.Certificate.MixedData.merged753part6 line 185
  59. def OAI.MUB6.Certificate.MixedData.merged753part7 line 187
  60. def OAI.MUB6.Certificate.MixedData.merged753 line 189
  61. theorem OAI.MUB6.Certificate.MixedData.mergeCheck753 line 191
  62. theorem OAI.MUB6.Certificate.MixedData.mergedZero753 line 193
  63. def OAI.MUB6.Certificate.MixedData.merged754part0 line 199
  64. def OAI.MUB6.Certificate.MixedData.merged754part1 line 201
  65. def OAI.MUB6.Certificate.MixedData.merged754part2 line 203
  66. def OAI.MUB6.Certificate.MixedData.merged754part3 line 205
  67. def OAI.MUB6.Certificate.MixedData.merged754part4 line 207
  68. def OAI.MUB6.Certificate.MixedData.merged754part5 line 209
  69. def OAI.MUB6.Certificate.MixedData.merged754part6 line 211
  70. def OAI.MUB6.Certificate.MixedData.merged754part7 line 213
  71. def OAI.MUB6.Certificate.MixedData.merged754part8 line 215
  72. def OAI.MUB6.Certificate.MixedData.merged754part9 line 217
  73. def OAI.MUB6.Certificate.MixedData.merged754part10 line 219
  74. def OAI.MUB6.Certificate.MixedData.merged754part11 line 221
  75. def OAI.MUB6.Certificate.MixedData.merged754 line 223
  76. theorem OAI.MUB6.Certificate.MixedData.mergeCheck754 line 225
  77. theorem OAI.MUB6.Certificate.MixedData.mergedZero754 line 227
  78. def OAI.MUB6.Certificate.MixedData.merged755 line 233
  79. theorem OAI.MUB6.Certificate.MixedData.mergeCheck755 line 235
  80. theorem OAI.MUB6.Certificate.MixedData.mergedZero755 line 237
  81. def OAI.MUB6.Certificate.MixedData.merged756 line 242
  82. theorem OAI.MUB6.Certificate.MixedData.mergeCheck756 line 244
  83. theorem OAI.MUB6.Certificate.MixedData.mergedZero756 line 246
  84. def OAI.MUB6.Certificate.MixedData.merged757 line 251
  85. theorem OAI.MUB6.Certificate.MixedData.mergeCheck757 line 253
  86. theorem OAI.MUB6.Certificate.MixedData.mergedZero757 line 255
  87. def OAI.MUB6.Certificate.MixedData.merged758 line 261
  88. theorem OAI.MUB6.Certificate.MixedData.mergeCheck758 line 263
  89. theorem OAI.MUB6.Certificate.MixedData.mergedZero758 line 265
  90. def OAI.MUB6.Certificate.MixedData.merged759 line 270
  91. theorem OAI.MUB6.Certificate.MixedData.mergeCheck759 line 272
  92. theorem OAI.MUB6.Certificate.MixedData.mergedZero759 line 274
  93. def OAI.MUB6.Certificate.MixedData.merged760 line 279
  94. theorem OAI.MUB6.Certificate.MixedData.mergeCheck760 line 281
  95. theorem OAI.MUB6.Certificate.MixedData.mergedZero760 line 283
  96. def OAI.MUB6.Certificate.MixedData.merged761 line 289
  97. theorem OAI.MUB6.Certificate.MixedData.mergeCheck761 line 291
  98. theorem OAI.MUB6.Certificate.MixedData.mergedZero761 line 293
  99. def OAI.MUB6.Certificate.MixedData.merged762 line 299
  100. theorem OAI.MUB6.Certificate.MixedData.mergeCheck762 line 301
  101. theorem OAI.MUB6.Certificate.MixedData.mergedZero762 line 303
  102. def OAI.MUB6.Certificate.MixedData.merged763 line 309
  103. theorem OAI.MUB6.Certificate.MixedData.mergeCheck763 line 311
  104. theorem OAI.MUB6.Certificate.MixedData.mergedZero763 line 313
  105. def OAI.MUB6.Certificate.MixedData.merged764 line 318
  106. theorem OAI.MUB6.Certificate.MixedData.mergeCheck764 line 320
  107. theorem OAI.MUB6.Certificate.MixedData.mergedZero764 line 322
  108. def OAI.MUB6.Certificate.MixedData.merged765 line 327
  109. theorem OAI.MUB6.Certificate.MixedData.mergeCheck765 line 329
  110. theorem OAI.MUB6.Certificate.MixedData.mergedZero765 line 331
  111. def OAI.MUB6.Certificate.MixedData.merged766 line 337
  112. theorem OAI.MUB6.Certificate.MixedData.mergeCheck766 line 339
  113. theorem OAI.MUB6.Certificate.MixedData.mergedZero766 line 341
  114. def OAI.MUB6.Certificate.MixedData.merged767 line 347
  115. theorem OAI.MUB6.Certificate.MixedData.mergeCheck767 line 349
  116. theorem OAI.MUB6.Certificate.MixedData.mergedZero767 line 351