OAI/Analysis/MutuallyUnbiased/MixedMerge/Block52.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1664 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1664 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1664 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1665 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1665 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1665 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged1666 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1666 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1666 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged1667 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1667 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1667 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged1668 line 46
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1668 line 48
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1668 line 50
  16. def OAI.MUB6.Certificate.MixedData.merged1669 line 56
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1669 line 58
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1669 line 60
  19. def OAI.MUB6.Certificate.MixedData.merged1670 line 66
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1670 line 68
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1670 line 70
  22. def OAI.MUB6.Certificate.MixedData.merged1671 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1671 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1671 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged1672 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1672 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1672 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged1673 line 94
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1673 line 96
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1673 line 98
  31. def OAI.MUB6.Certificate.MixedData.merged1674 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1674 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1674 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged1675 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1675 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1675 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged1676 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1676 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1676 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged1677 line 132
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1677 line 134
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1677 line 136
  43. def OAI.MUB6.Certificate.MixedData.merged1678 line 142
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1678 line 144
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1678 line 146
  46. def OAI.MUB6.Certificate.MixedData.merged1679 line 152
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1679 line 154
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1679 line 156
  49. def OAI.MUB6.Certificate.MixedData.merged1680 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1680 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1680 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged1681 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1681 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1681 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged1682 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1682 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1682 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged1683 line 190
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1683 line 192
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1683 line 194
  61. def OAI.MUB6.Certificate.MixedData.merged1684 line 200
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1684 line 202
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1684 line 204
  64. def OAI.MUB6.Certificate.MixedData.merged1685 line 209
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1685 line 211
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1685 line 213
  67. def OAI.MUB6.Certificate.MixedData.merged1686 line 218
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1686 line 220
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1686 line 222
  70. def OAI.MUB6.Certificate.MixedData.merged1687 line 228
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1687 line 230
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1687 line 232
  73. def OAI.MUB6.Certificate.MixedData.merged1688 line 238
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1688 line 240
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1688 line 242
  76. def OAI.MUB6.Certificate.MixedData.merged1689 line 248
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1689 line 250
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1689 line 252
  79. def OAI.MUB6.Certificate.MixedData.merged1690 line 257
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1690 line 259
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1690 line 261
  82. def OAI.MUB6.Certificate.MixedData.merged1691 line 266
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1691 line 268
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero1691 line 270
  85. def OAI.MUB6.Certificate.MixedData.merged1692 line 276
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1692 line 278
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero1692 line 280
  88. def OAI.MUB6.Certificate.MixedData.merged1693 line 286
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1693 line 288
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero1693 line 290
  91. def OAI.MUB6.Certificate.MixedData.merged1694 line 295
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1694 line 297
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero1694 line 299
  94. def OAI.MUB6.Certificate.MixedData.merged1695 line 304
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1695 line 306
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero1695 line 308