OAI/Analysis/MutuallyUnbiased/MixedMerge/Block46.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1472 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1472 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1472 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1473 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1473 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1473 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged1474 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1474 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1474 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged1475 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1475 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1475 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged1476 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1476 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1476 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged1477 line 56
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1477 line 58
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1477 line 60
  19. def OAI.MUB6.Certificate.MixedData.merged1478 line 65
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1478 line 67
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1478 line 69
  22. def OAI.MUB6.Certificate.MixedData.merged1479 line 75
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1479 line 77
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1479 line 79
  25. def OAI.MUB6.Certificate.MixedData.merged1480 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1480 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1480 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged1481 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1481 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1481 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged1482 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1482 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1482 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged1483 line 113
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1483 line 115
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1483 line 117
  37. def OAI.MUB6.Certificate.MixedData.merged1484 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1484 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1484 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged1485 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1485 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1485 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged1486 line 142
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1486 line 144
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1486 line 146
  46. def OAI.MUB6.Certificate.MixedData.merged1487 line 151
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1487 line 153
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1487 line 155
  49. def OAI.MUB6.Certificate.MixedData.merged1488 line 161
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1488 line 163
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1488 line 165
  52. def OAI.MUB6.Certificate.MixedData.merged1489 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1489 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1489 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged1490 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1490 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1490 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged1491 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1491 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1491 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged1492 line 200
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1492 line 202
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1492 line 204
  64. def OAI.MUB6.Certificate.MixedData.merged1493 line 209
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1493 line 211
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1493 line 213
  67. def OAI.MUB6.Certificate.MixedData.merged1494 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1494 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1494 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged1495 line 228
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1495 line 230
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1495 line 232
  73. def OAI.MUB6.Certificate.MixedData.merged1496 line 237
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1496 line 239
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1496 line 241
  76. def OAI.MUB6.Certificate.MixedData.merged1497 line 247
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1497 line 249
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1497 line 251
  79. def OAI.MUB6.Certificate.MixedData.merged1498 line 257
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1498 line 259
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1498 line 261
  82. def OAI.MUB6.Certificate.MixedData.merged1499 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1499 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero1499 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged1500 line 276
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1500 line 278
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero1500 line 280
  88. def OAI.MUB6.Certificate.MixedData.merged1501 line 285
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1501 line 287
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero1501 line 289
  91. def OAI.MUB6.Certificate.MixedData.merged1502 line 295
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1502 line 297
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero1502 line 299
  94. def OAI.MUB6.Certificate.MixedData.merged1503 line 305
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1503 line 307
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero1503 line 309