OAI/Analysis/MutuallyUnbiased/MixedMerge/Block48.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1536 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1536 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1536 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1537 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1537 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1537 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged1538 line 29
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1538 line 31
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1538 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged1539 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1539 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1539 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged1540 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1540 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1540 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged1541 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1541 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1541 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged1542 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1542 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1542 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged1543 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1543 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1543 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged1544 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1544 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1544 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged1545 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1545 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1545 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged1546 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1546 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1546 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged1547 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1547 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1547 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged1548 line 125
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1548 line 127
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1548 line 129
  40. def OAI.MUB6.Certificate.MixedData.merged1549 line 135
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1549 line 137
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1549 line 139
  43. def OAI.MUB6.Certificate.MixedData.merged1550 line 144
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1550 line 146
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1550 line 148
  46. def OAI.MUB6.Certificate.MixedData.merged1551 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1551 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1551 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged1552 line 163
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1552 line 165
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1552 line 167
  52. def OAI.MUB6.Certificate.MixedData.merged1553 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1553 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1553 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged1554 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1554 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1554 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged1555 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1555 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1555 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged1556 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1556 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1556 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged1557 line 211
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1557 line 213
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1557 line 215
  67. def OAI.MUB6.Certificate.MixedData.merged1558 line 220
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1558 line 222
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1558 line 224
  70. def OAI.MUB6.Certificate.MixedData.merged1559 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1559 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1559 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged1560 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1560 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1560 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged1561 line 249
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1561 line 251
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1561 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged1562 line 258
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1562 line 260
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1562 line 262
  82. def OAI.MUB6.Certificate.MixedData.merged1563 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1563 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero1563 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged1564 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1564 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero1564 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged1565 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1565 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero1565 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged1566 line 297
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1566 line 299
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero1566 line 301
  94. def OAI.MUB6.Certificate.MixedData.merged1567 line 307
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1567 line 309
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero1567 line 311