OAI/Analysis/MutuallyUnbiased/MixedMerge/Block19.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged608 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck608 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero608 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged609 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck609 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero609 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged610 line 27
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck610 line 29
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero610 line 31
  10. def OAI.MUB6.Certificate.MixedData.merged611 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck611 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero611 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged612 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck612 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero612 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged613 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck613 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero613 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged614 line 66
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck614 line 68
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero614 line 70
  22. def OAI.MUB6.Certificate.MixedData.merged615 line 75
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck615 line 77
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero615 line 79
  25. def OAI.MUB6.Certificate.MixedData.merged616 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck616 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero616 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged617 line 94
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck617 line 96
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero617 line 98
  31. def OAI.MUB6.Certificate.MixedData.merged618 line 103
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck618 line 105
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero618 line 107
  34. def OAI.MUB6.Certificate.MixedData.merged619 line 113
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck619 line 115
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero619 line 117
  37. def OAI.MUB6.Certificate.MixedData.merged620 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck620 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero620 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged621 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck621 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero621 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged622 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck622 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero622 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged623 line 152
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck623 line 154
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero623 line 156
  49. def OAI.MUB6.Certificate.MixedData.merged624 line 161
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck624 line 163
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero624 line 165
  52. def OAI.MUB6.Certificate.MixedData.merged625 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck625 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero625 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged626 line 180
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck626 line 182
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero626 line 184
  58. def OAI.MUB6.Certificate.MixedData.merged627 line 189
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck627 line 191
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero627 line 193
  61. def OAI.MUB6.Certificate.MixedData.merged628 line 199
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck628 line 201
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero628 line 203
  64. def OAI.MUB6.Certificate.MixedData.merged629 line 209
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck629 line 211
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero629 line 213
  67. def OAI.MUB6.Certificate.MixedData.merged630 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck630 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero630 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged631 line 228
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck631 line 230
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero631 line 232
  73. def OAI.MUB6.Certificate.MixedData.merged632 line 237
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck632 line 239
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero632 line 241
  76. def OAI.MUB6.Certificate.MixedData.merged633 line 247
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck633 line 249
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero633 line 251
  79. def OAI.MUB6.Certificate.MixedData.merged634 line 257
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck634 line 259
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero634 line 261
  82. def OAI.MUB6.Certificate.MixedData.merged635 line 266
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck635 line 268
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero635 line 270
  85. def OAI.MUB6.Certificate.MixedData.merged636 line 275
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck636 line 277
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero636 line 279
  88. def OAI.MUB6.Certificate.MixedData.merged637 line 285
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck637 line 287
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero637 line 289
  91. def OAI.MUB6.Certificate.MixedData.merged638 line 295
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck638 line 297
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero638 line 299
  94. def OAI.MUB6.Certificate.MixedData.merged639 line 305
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck639 line 307
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero639 line 309