OAI/Analysis/MutuallyUnbiased/MixedMerge/Block49.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1568 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1568 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1568 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1569 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1569 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1569 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged1570 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1570 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1570 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged1571 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1571 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1571 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged1572 line 46
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1572 line 48
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1572 line 50
  16. def OAI.MUB6.Certificate.MixedData.merged1573 line 56
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1573 line 58
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1573 line 60
  19. def OAI.MUB6.Certificate.MixedData.merged1574 line 66
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1574 line 68
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1574 line 70
  22. def OAI.MUB6.Certificate.MixedData.merged1575 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1575 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1575 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged1576 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1576 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1576 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged1577 line 94
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1577 line 96
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1577 line 98
  31. def OAI.MUB6.Certificate.MixedData.merged1578 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1578 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1578 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged1579 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1579 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1579 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged1580 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1580 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1580 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged1581 line 132
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1581 line 134
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1581 line 136
  43. def OAI.MUB6.Certificate.MixedData.merged1582 line 142
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1582 line 144
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1582 line 146
  46. def OAI.MUB6.Certificate.MixedData.merged1583 line 152
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1583 line 154
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1583 line 156
  49. def OAI.MUB6.Certificate.MixedData.merged1584 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1584 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1584 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged1585 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1585 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1585 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged1586 line 182
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1586 line 184
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1586 line 186
  58. def OAI.MUB6.Certificate.MixedData.merged1587 line 192
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1587 line 194
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1587 line 196
  61. def OAI.MUB6.Certificate.MixedData.merged1588 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1588 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1588 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged1589 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1589 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1589 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged1590 line 220
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1590 line 222
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1590 line 224
  70. def OAI.MUB6.Certificate.MixedData.merged1591 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1591 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1591 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged1592 line 238
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1592 line 240
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1592 line 242
  76. def OAI.MUB6.Certificate.MixedData.merged1593 line 248
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1593 line 250
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1593 line 252
  79. def OAI.MUB6.Certificate.MixedData.merged1594 line 258
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1594 line 260
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1594 line 262
  82. def OAI.MUB6.Certificate.MixedData.merged1595 line 268
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1595 line 270
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero1595 line 272
  85. def OAI.MUB6.Certificate.MixedData.merged1596 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1596 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero1596 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged1597 line 286
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1597 line 288
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero1597 line 290
  91. def OAI.MUB6.Certificate.MixedData.merged1598 line 296
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1598 line 298
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero1598 line 300
  94. def OAI.MUB6.Certificate.MixedData.merged1599 line 306
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1599 line 308
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero1599 line 310