OAI/Analysis/MutuallyUnbiased/MixedMerge/Block51.lean

GitHub source file

115 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1632 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1632 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1632 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1633 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1633 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1633 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged1634 line 27
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1634 line 29
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1634 line 31
  10. def OAI.MUB6.Certificate.MixedData.merged1635 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1635 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1635 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged1636 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1636 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1636 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged1637 line 56
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1637 line 58
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1637 line 60
  19. def OAI.MUB6.Certificate.MixedData.merged1638 line 65
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1638 line 67
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1638 line 69
  22. def OAI.MUB6.Certificate.MixedData.merged1639 line 75
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1639 line 77
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1639 line 79
  25. def OAI.MUB6.Certificate.MixedData.merged1640 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1640 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1640 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged1641 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1641 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1641 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged1642 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1642 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1642 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged1643 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1643 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1643 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged1644 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1644 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1644 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged1645 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1645 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1645 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged1646 line 142
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1646 line 144
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1646 line 146
  46. def OAI.MUB6.Certificate.MixedData.merged1647 line 151
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1647 line 153
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1647 line 155
  49. def OAI.MUB6.Certificate.MixedData.merged1648 line 161
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1648 line 163
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1648 line 165
  52. def OAI.MUB6.Certificate.MixedData.merged1649 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1649 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1649 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged1650 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1650 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1650 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged1651 line 190
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1651 line 192
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1651 line 194
  61. def OAI.MUB6.Certificate.MixedData.merged1652 line 199
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1652 line 201
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1652 line 203
  64. def OAI.MUB6.Certificate.MixedData.merged1653 line 209
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1653 line 211
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1653 line 213
  67. def OAI.MUB6.Certificate.MixedData.merged1654 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1654 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1654 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged1655 line 228
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1655 line 230
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1655 line 232
  73. def OAI.MUB6.Certificate.MixedData.merged1656 line 237
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1656 line 239
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1656 line 241
  76. def OAI.MUB6.Certificate.MixedData.merged1657 line 247
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1657 line 249
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1657 line 251
  79. def OAI.MUB6.Certificate.MixedData.merged1658 line 257
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1658 line 259
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1658 line 261
  82. def OAI.MUB6.Certificate.MixedData.merged1659 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1659 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero1659 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged1660 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1660 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero1660 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged1661part0 line 287
  89. def OAI.MUB6.Certificate.MixedData.merged1661part1 line 289
  90. def OAI.MUB6.Certificate.MixedData.merged1661part2 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged1661part3 line 293
  92. def OAI.MUB6.Certificate.MixedData.merged1661part4 line 295
  93. def OAI.MUB6.Certificate.MixedData.merged1661part5 line 297
  94. def OAI.MUB6.Certificate.MixedData.merged1661part6 line 299
  95. def OAI.MUB6.Certificate.MixedData.merged1661part7 line 301
  96. def OAI.MUB6.Certificate.MixedData.merged1661 line 303
  97. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1661 line 305
  98. theorem OAI.MUB6.Certificate.MixedData.mergedZero1661 line 307
  99. def OAI.MUB6.Certificate.MixedData.merged1662part0 line 313
  100. def OAI.MUB6.Certificate.MixedData.merged1662part1 line 315
  101. def OAI.MUB6.Certificate.MixedData.merged1662part2 line 317
  102. def OAI.MUB6.Certificate.MixedData.merged1662part3 line 319
  103. def OAI.MUB6.Certificate.MixedData.merged1662part4 line 321
  104. def OAI.MUB6.Certificate.MixedData.merged1662part5 line 323
  105. def OAI.MUB6.Certificate.MixedData.merged1662part6 line 325
  106. def OAI.MUB6.Certificate.MixedData.merged1662part7 line 327
  107. def OAI.MUB6.Certificate.MixedData.merged1662part8 line 329
  108. def OAI.MUB6.Certificate.MixedData.merged1662part9 line 331
  109. def OAI.MUB6.Certificate.MixedData.merged1662part10 line 333
  110. def OAI.MUB6.Certificate.MixedData.merged1662 line 335
  111. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1662 line 337
  112. theorem OAI.MUB6.Certificate.MixedData.mergedZero1662 line 339
  113. def OAI.MUB6.Certificate.MixedData.merged1663 line 345
  114. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1663 line 347
  115. theorem OAI.MUB6.Certificate.MixedData.mergedZero1663 line 349