OAI/Analysis/MutuallyUnbiased/MixedMerge/Block57.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1824 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1824 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1824 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1825 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1825 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1825 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged1826 line 27
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1826 line 29
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1826 line 31
  10. def OAI.MUB6.Certificate.MixedData.merged1827 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1827 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1827 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged1828 line 46
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1828 line 48
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1828 line 50
  16. def OAI.MUB6.Certificate.MixedData.merged1829 line 55
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1829 line 57
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1829 line 59
  19. def OAI.MUB6.Certificate.MixedData.merged1830 line 65
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1830 line 67
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1830 line 69
  22. def OAI.MUB6.Certificate.MixedData.merged1831 line 75
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1831 line 77
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1831 line 79
  25. def OAI.MUB6.Certificate.MixedData.merged1832 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1832 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1832 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged1833 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1833 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1833 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged1834 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1834 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1834 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged1835 line 113
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1835 line 115
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1835 line 117
  37. def OAI.MUB6.Certificate.MixedData.merged1836 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1836 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1836 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged1837 line 132
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1837 line 134
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1837 line 136
  43. def OAI.MUB6.Certificate.MixedData.merged1838 line 141
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1838 line 143
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1838 line 145
  46. def OAI.MUB6.Certificate.MixedData.merged1839 line 151
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1839 line 153
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1839 line 155
  49. def OAI.MUB6.Certificate.MixedData.merged1840 line 161
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1840 line 163
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1840 line 165
  52. def OAI.MUB6.Certificate.MixedData.merged1841 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1841 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1841 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged1842 line 180
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1842 line 182
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1842 line 184
  58. def OAI.MUB6.Certificate.MixedData.merged1843 line 189
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1843 line 191
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1843 line 193
  61. def OAI.MUB6.Certificate.MixedData.merged1844 line 199
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1844 line 201
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1844 line 203
  64. def OAI.MUB6.Certificate.MixedData.merged1845 line 209
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1845 line 211
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1845 line 213
  67. def OAI.MUB6.Certificate.MixedData.merged1846 line 218
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1846 line 220
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1846 line 222
  70. def OAI.MUB6.Certificate.MixedData.merged1847 line 227
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1847 line 229
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1847 line 231
  73. def OAI.MUB6.Certificate.MixedData.merged1848 line 237
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1848 line 239
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1848 line 241
  76. def OAI.MUB6.Certificate.MixedData.merged1849 line 247
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1849 line 249
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1849 line 251
  79. def OAI.MUB6.Certificate.MixedData.merged1850 line 257
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1850 line 259
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1850 line 261
  82. def OAI.MUB6.Certificate.MixedData.merged1851part0 line 267
  83. def OAI.MUB6.Certificate.MixedData.merged1851part1 line 269
  84. def OAI.MUB6.Certificate.MixedData.merged1851part2 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged1851part3 line 273
  86. def OAI.MUB6.Certificate.MixedData.merged1851part4 line 275
  87. def OAI.MUB6.Certificate.MixedData.merged1851part5 line 277
  88. def OAI.MUB6.Certificate.MixedData.merged1851part6 line 279
  89. def OAI.MUB6.Certificate.MixedData.merged1851part7 line 281
  90. def OAI.MUB6.Certificate.MixedData.merged1851 line 283
  91. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1851 line 285
  92. theorem OAI.MUB6.Certificate.MixedData.mergedZero1851 line 287
  93. def OAI.MUB6.Certificate.MixedData.merged1852 line 293
  94. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1852 line 295
  95. theorem OAI.MUB6.Certificate.MixedData.mergedZero1852 line 297
  96. def OAI.MUB6.Certificate.MixedData.merged1853 line 302
  97. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1853 line 304
  98. theorem OAI.MUB6.Certificate.MixedData.mergedZero1853 line 306
  99. def OAI.MUB6.Certificate.MixedData.merged1854 line 311
  100. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1854 line 313
  101. theorem OAI.MUB6.Certificate.MixedData.mergedZero1854 line 315
  102. def OAI.MUB6.Certificate.MixedData.merged1855 line 321
  103. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1855 line 323
  104. theorem OAI.MUB6.Certificate.MixedData.mergedZero1855 line 325