OAI/Analysis/MutuallyUnbiased/MixedMerge/Block55.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1760 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1760 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1760 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1761 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1761 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1761 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged1762 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1762 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1762 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged1763 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1763 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1763 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged1764 line 48
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1764 line 50
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1764 line 52
  16. def OAI.MUB6.Certificate.MixedData.merged1765 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1765 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1765 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged1766 line 66
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1766 line 68
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1766 line 70
  22. def OAI.MUB6.Certificate.MixedData.merged1767 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1767 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1767 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged1768 line 86
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1768 line 88
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1768 line 90
  28. def OAI.MUB6.Certificate.MixedData.merged1769 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1769 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1769 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged1770 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1770 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1770 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged1771 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1771 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1771 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged1772 line 124
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1772 line 126
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1772 line 128
  40. def OAI.MUB6.Certificate.MixedData.merged1773 line 134
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1773 line 136
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1773 line 138
  43. def OAI.MUB6.Certificate.MixedData.merged1774 line 144
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1774 line 146
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1774 line 148
  46. def OAI.MUB6.Certificate.MixedData.merged1775 line 154
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1775 line 156
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1775 line 158
  49. def OAI.MUB6.Certificate.MixedData.merged1776 line 163
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1776 line 165
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1776 line 167
  52. def OAI.MUB6.Certificate.MixedData.merged1777 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1777 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1777 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged1778 line 182
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1778 line 184
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1778 line 186
  58. def OAI.MUB6.Certificate.MixedData.merged1779 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1779 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1779 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged1780 line 200
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1780 line 202
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1780 line 204
  64. def OAI.MUB6.Certificate.MixedData.merged1781 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1781 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1781 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged1782 line 220
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1782 line 222
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1782 line 224
  70. def OAI.MUB6.Certificate.MixedData.merged1783 line 230
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1783 line 232
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1783 line 234
  73. def OAI.MUB6.Certificate.MixedData.merged1784 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1784 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1784 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged1785 line 248
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1785 line 250
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1785 line 252
  79. def OAI.MUB6.Certificate.MixedData.merged1786 line 258
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1786 line 260
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1786 line 262
  82. def OAI.MUB6.Certificate.MixedData.merged1787 line 268
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1787 line 270
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero1787 line 272
  85. def OAI.MUB6.Certificate.MixedData.merged1788 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1788 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero1788 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged1789 line 286
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1789 line 288
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero1789 line 290
  91. def OAI.MUB6.Certificate.MixedData.merged1790 line 296
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1790 line 298
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero1790 line 300
  94. def OAI.MUB6.Certificate.MixedData.merged1791 line 306
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1791 line 308
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero1791 line 310