OAI/Analysis/MutuallyUnbiased/MixedMerge/Block50.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1600 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1600 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1600 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1601 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1601 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1601 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged1602 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1602 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1602 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged1603 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1603 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1603 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged1604 line 48
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1604 line 50
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1604 line 52
  16. def OAI.MUB6.Certificate.MixedData.merged1605 line 58
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1605 line 60
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1605 line 62
  19. def OAI.MUB6.Certificate.MixedData.merged1606 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1606 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1606 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged1607 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1607 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1607 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged1608 line 86
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1608 line 88
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1608 line 90
  28. def OAI.MUB6.Certificate.MixedData.merged1609 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1609 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1609 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged1610 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1610 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1610 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged1611 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1611 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1611 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged1612 line 124
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1612 line 126
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1612 line 128
  40. def OAI.MUB6.Certificate.MixedData.merged1613 line 134
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1613 line 136
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1613 line 138
  43. def OAI.MUB6.Certificate.MixedData.merged1614 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1614 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1614 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged1615 line 152
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1615 line 154
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1615 line 156
  49. def OAI.MUB6.Certificate.MixedData.merged1616 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1616 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1616 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged1617 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1617 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1617 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged1618 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1618 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1618 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged1619 line 190
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1619 line 192
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1619 line 194
  61. def OAI.MUB6.Certificate.MixedData.merged1620 line 200
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1620 line 202
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1620 line 204
  64. def OAI.MUB6.Certificate.MixedData.merged1621 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1621 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1621 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged1622 line 220
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1622 line 222
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1622 line 224
  70. def OAI.MUB6.Certificate.MixedData.merged1623 line 230
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1623 line 232
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1623 line 234
  73. def OAI.MUB6.Certificate.MixedData.merged1624 line 240
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1624 line 242
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1624 line 244
  76. def OAI.MUB6.Certificate.MixedData.merged1625 line 249
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1625 line 251
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1625 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged1626 line 258
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1626 line 260
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1626 line 262
  82. def OAI.MUB6.Certificate.MixedData.merged1627 line 268
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1627 line 270
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero1627 line 272
  85. def OAI.MUB6.Certificate.MixedData.merged1628 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1628 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero1628 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged1629 line 286
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1629 line 288
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero1629 line 290
  91. def OAI.MUB6.Certificate.MixedData.merged1630 line 296
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1630 line 298
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero1630 line 300
  94. def OAI.MUB6.Certificate.MixedData.merged1631 line 306
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1631 line 308
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero1631 line 310