OAI/Analysis/MutuallyUnbiased/MixedMerge/Block54.lean

GitHub source file

107 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1728 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1728 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1728 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1729 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1729 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1729 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged1730 line 29
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1730 line 31
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1730 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged1731 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1731 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1731 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged1732 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1732 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1732 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged1733 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1733 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1733 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged1734 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1734 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1734 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged1735 line 77
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1735 line 79
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1735 line 81
  25. def OAI.MUB6.Certificate.MixedData.merged1736 line 87
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1736 line 89
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1736 line 91
  28. def OAI.MUB6.Certificate.MixedData.merged1737part0 line 97
  29. def OAI.MUB6.Certificate.MixedData.merged1737part1 line 99
  30. def OAI.MUB6.Certificate.MixedData.merged1737part2 line 101
  31. def OAI.MUB6.Certificate.MixedData.merged1737part3 line 103
  32. def OAI.MUB6.Certificate.MixedData.merged1737part4 line 105
  33. def OAI.MUB6.Certificate.MixedData.merged1737part5 line 107
  34. def OAI.MUB6.Certificate.MixedData.merged1737part6 line 109
  35. def OAI.MUB6.Certificate.MixedData.merged1737part7 line 111
  36. def OAI.MUB6.Certificate.MixedData.merged1737part8 line 113
  37. def OAI.MUB6.Certificate.MixedData.merged1737part9 line 115
  38. def OAI.MUB6.Certificate.MixedData.merged1737part10 line 117
  39. def OAI.MUB6.Certificate.MixedData.merged1737 line 119
  40. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1737 line 121
  41. theorem OAI.MUB6.Certificate.MixedData.mergedZero1737 line 123
  42. def OAI.MUB6.Certificate.MixedData.merged1738 line 129
  43. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1738 line 131
  44. theorem OAI.MUB6.Certificate.MixedData.mergedZero1738 line 133
  45. def OAI.MUB6.Certificate.MixedData.merged1739 line 138
  46. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1739 line 140
  47. theorem OAI.MUB6.Certificate.MixedData.mergedZero1739 line 142
  48. def OAI.MUB6.Certificate.MixedData.merged1740 line 147
  49. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1740 line 149
  50. theorem OAI.MUB6.Certificate.MixedData.mergedZero1740 line 151
  51. def OAI.MUB6.Certificate.MixedData.merged1741 line 157
  52. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1741 line 159
  53. theorem OAI.MUB6.Certificate.MixedData.mergedZero1741 line 161
  54. def OAI.MUB6.Certificate.MixedData.merged1742 line 166
  55. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1742 line 168
  56. theorem OAI.MUB6.Certificate.MixedData.mergedZero1742 line 170
  57. def OAI.MUB6.Certificate.MixedData.merged1743 line 175
  58. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1743 line 177
  59. theorem OAI.MUB6.Certificate.MixedData.mergedZero1743 line 179
  60. def OAI.MUB6.Certificate.MixedData.merged1744 line 185
  61. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1744 line 187
  62. theorem OAI.MUB6.Certificate.MixedData.mergedZero1744 line 189
  63. def OAI.MUB6.Certificate.MixedData.merged1745 line 195
  64. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1745 line 197
  65. theorem OAI.MUB6.Certificate.MixedData.mergedZero1745 line 199
  66. def OAI.MUB6.Certificate.MixedData.merged1746 line 205
  67. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1746 line 207
  68. theorem OAI.MUB6.Certificate.MixedData.mergedZero1746 line 209
  69. def OAI.MUB6.Certificate.MixedData.merged1747 line 214
  70. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1747 line 216
  71. theorem OAI.MUB6.Certificate.MixedData.mergedZero1747 line 218
  72. def OAI.MUB6.Certificate.MixedData.merged1748 line 223
  73. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1748 line 225
  74. theorem OAI.MUB6.Certificate.MixedData.mergedZero1748 line 227
  75. def OAI.MUB6.Certificate.MixedData.merged1749 line 233
  76. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1749 line 235
  77. theorem OAI.MUB6.Certificate.MixedData.mergedZero1749 line 237
  78. def OAI.MUB6.Certificate.MixedData.merged1750 line 243
  79. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1750 line 245
  80. theorem OAI.MUB6.Certificate.MixedData.mergedZero1750 line 247
  81. def OAI.MUB6.Certificate.MixedData.merged1751 line 252
  82. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1751 line 254
  83. theorem OAI.MUB6.Certificate.MixedData.mergedZero1751 line 256
  84. def OAI.MUB6.Certificate.MixedData.merged1752 line 261
  85. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1752 line 263
  86. theorem OAI.MUB6.Certificate.MixedData.mergedZero1752 line 265
  87. def OAI.MUB6.Certificate.MixedData.merged1753 line 271
  88. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1753 line 273
  89. theorem OAI.MUB6.Certificate.MixedData.mergedZero1753 line 275
  90. def OAI.MUB6.Certificate.MixedData.merged1754 line 281
  91. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1754 line 283
  92. theorem OAI.MUB6.Certificate.MixedData.mergedZero1754 line 285
  93. def OAI.MUB6.Certificate.MixedData.merged1755 line 291
  94. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1755 line 293
  95. theorem OAI.MUB6.Certificate.MixedData.mergedZero1755 line 295
  96. def OAI.MUB6.Certificate.MixedData.merged1756 line 301
  97. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1756 line 303
  98. theorem OAI.MUB6.Certificate.MixedData.mergedZero1756 line 305
  99. def OAI.MUB6.Certificate.MixedData.merged1757 line 310
  100. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1757 line 312
  101. theorem OAI.MUB6.Certificate.MixedData.mergedZero1757 line 314
  102. def OAI.MUB6.Certificate.MixedData.merged1758 line 319
  103. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1758 line 321
  104. theorem OAI.MUB6.Certificate.MixedData.mergedZero1758 line 323
  105. def OAI.MUB6.Certificate.MixedData.merged1759 line 329
  106. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1759 line 331
  107. theorem OAI.MUB6.Certificate.MixedData.mergedZero1759 line 333