OAI/Analysis/MutuallyUnbiased/MixedMerge/Block45.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1440 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1440 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1440 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1441 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1441 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1441 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged1442 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1442 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1442 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged1443 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1443 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1443 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged1444 line 48
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1444 line 50
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1444 line 52
  16. def OAI.MUB6.Certificate.MixedData.merged1445 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1445 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1445 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged1446 line 66
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1446 line 68
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1446 line 70
  22. def OAI.MUB6.Certificate.MixedData.merged1447 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1447 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1447 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged1448 line 86
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1448 line 88
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1448 line 90
  28. def OAI.MUB6.Certificate.MixedData.merged1449 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1449 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1449 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged1450 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1450 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1450 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged1451 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1451 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1451 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged1452 line 124
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1452 line 126
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1452 line 128
  40. def OAI.MUB6.Certificate.MixedData.merged1453 line 134
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1453 line 136
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1453 line 138
  43. def OAI.MUB6.Certificate.MixedData.merged1454 line 144
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1454 line 146
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1454 line 148
  46. def OAI.MUB6.Certificate.MixedData.merged1455 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1455 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1455 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged1456 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1456 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1456 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged1457 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1457 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1457 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged1458 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1458 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1458 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged1459 line 190
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1459 line 192
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1459 line 194
  61. def OAI.MUB6.Certificate.MixedData.merged1460 line 200
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1460 line 202
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1460 line 204
  64. def OAI.MUB6.Certificate.MixedData.merged1461 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1461 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1461 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged1462 line 220
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1462 line 222
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1462 line 224
  70. def OAI.MUB6.Certificate.MixedData.merged1463 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1463 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1463 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged1464 line 238
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1464 line 240
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1464 line 242
  76. def OAI.MUB6.Certificate.MixedData.merged1465 line 248
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1465 line 250
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1465 line 252
  79. def OAI.MUB6.Certificate.MixedData.merged1466 line 258
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1466 line 260
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1466 line 262
  82. def OAI.MUB6.Certificate.MixedData.merged1467 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1467 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero1467 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged1468 line 276
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1468 line 278
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero1468 line 280
  88. def OAI.MUB6.Certificate.MixedData.merged1469 line 286
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1469 line 288
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero1469 line 290
  91. def OAI.MUB6.Certificate.MixedData.merged1470 line 296
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1470 line 298
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero1470 line 300
  94. def OAI.MUB6.Certificate.MixedData.merged1471 line 306
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1471 line 308
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero1471 line 310