OAI/Analysis/MutuallyUnbiased/MixedMerge/Block16.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged512 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck512 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero512 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged513 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck513 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero513 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged514 line 29
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck514 line 31
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero514 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged515 line 39
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck515 line 41
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero515 line 43
  13. def OAI.MUB6.Certificate.MixedData.merged516 line 48
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck516 line 50
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero516 line 52
  16. def OAI.MUB6.Certificate.MixedData.merged517 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck517 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero517 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged518 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck518 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero518 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged519 line 77
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck519 line 79
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero519 line 81
  25. def OAI.MUB6.Certificate.MixedData.merged520 line 86
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck520 line 88
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero520 line 90
  28. def OAI.MUB6.Certificate.MixedData.merged521 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck521 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero521 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged522 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck522 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero522 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged523 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck523 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero523 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged524 line 125
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck524 line 127
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero524 line 129
  40. def OAI.MUB6.Certificate.MixedData.merged525 line 135
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck525 line 137
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero525 line 139
  43. def OAI.MUB6.Certificate.MixedData.merged526part0 line 145
  44. def OAI.MUB6.Certificate.MixedData.merged526part1 line 147
  45. def OAI.MUB6.Certificate.MixedData.merged526part2 line 149
  46. def OAI.MUB6.Certificate.MixedData.merged526part3 line 151
  47. def OAI.MUB6.Certificate.MixedData.merged526part4 line 153
  48. def OAI.MUB6.Certificate.MixedData.merged526part5 line 155
  49. def OAI.MUB6.Certificate.MixedData.merged526part6 line 157
  50. def OAI.MUB6.Certificate.MixedData.merged526part7 line 159
  51. def OAI.MUB6.Certificate.MixedData.merged526 line 161
  52. theorem OAI.MUB6.Certificate.MixedData.mergeCheck526 line 163
  53. theorem OAI.MUB6.Certificate.MixedData.mergedZero526 line 165
  54. def OAI.MUB6.Certificate.MixedData.merged527 line 171
  55. theorem OAI.MUB6.Certificate.MixedData.mergeCheck527 line 173
  56. theorem OAI.MUB6.Certificate.MixedData.mergedZero527 line 175
  57. def OAI.MUB6.Certificate.MixedData.merged528 line 180
  58. theorem OAI.MUB6.Certificate.MixedData.mergeCheck528 line 182
  59. theorem OAI.MUB6.Certificate.MixedData.mergedZero528 line 184
  60. def OAI.MUB6.Certificate.MixedData.merged529 line 189
  61. theorem OAI.MUB6.Certificate.MixedData.mergeCheck529 line 191
  62. theorem OAI.MUB6.Certificate.MixedData.mergedZero529 line 193
  63. def OAI.MUB6.Certificate.MixedData.merged530 line 199
  64. theorem OAI.MUB6.Certificate.MixedData.mergeCheck530 line 201
  65. theorem OAI.MUB6.Certificate.MixedData.mergedZero530 line 203
  66. def OAI.MUB6.Certificate.MixedData.merged531 line 208
  67. theorem OAI.MUB6.Certificate.MixedData.mergeCheck531 line 210
  68. theorem OAI.MUB6.Certificate.MixedData.mergedZero531 line 212
  69. def OAI.MUB6.Certificate.MixedData.merged532 line 217
  70. theorem OAI.MUB6.Certificate.MixedData.mergeCheck532 line 219
  71. theorem OAI.MUB6.Certificate.MixedData.mergedZero532 line 221
  72. def OAI.MUB6.Certificate.MixedData.merged533 line 227
  73. theorem OAI.MUB6.Certificate.MixedData.mergeCheck533 line 229
  74. theorem OAI.MUB6.Certificate.MixedData.mergedZero533 line 231
  75. def OAI.MUB6.Certificate.MixedData.merged534 line 237
  76. theorem OAI.MUB6.Certificate.MixedData.mergeCheck534 line 239
  77. theorem OAI.MUB6.Certificate.MixedData.mergedZero534 line 241
  78. def OAI.MUB6.Certificate.MixedData.merged535 line 247
  79. theorem OAI.MUB6.Certificate.MixedData.mergeCheck535 line 249
  80. theorem OAI.MUB6.Certificate.MixedData.mergedZero535 line 251
  81. def OAI.MUB6.Certificate.MixedData.merged536 line 256
  82. theorem OAI.MUB6.Certificate.MixedData.mergeCheck536 line 258
  83. theorem OAI.MUB6.Certificate.MixedData.mergedZero536 line 260
  84. def OAI.MUB6.Certificate.MixedData.merged537 line 265
  85. theorem OAI.MUB6.Certificate.MixedData.mergeCheck537 line 267
  86. theorem OAI.MUB6.Certificate.MixedData.mergedZero537 line 269
  87. def OAI.MUB6.Certificate.MixedData.merged538 line 275
  88. theorem OAI.MUB6.Certificate.MixedData.mergeCheck538 line 277
  89. theorem OAI.MUB6.Certificate.MixedData.mergedZero538 line 279
  90. def OAI.MUB6.Certificate.MixedData.merged539 line 285
  91. theorem OAI.MUB6.Certificate.MixedData.mergeCheck539 line 287
  92. theorem OAI.MUB6.Certificate.MixedData.mergedZero539 line 289
  93. def OAI.MUB6.Certificate.MixedData.merged540 line 294
  94. theorem OAI.MUB6.Certificate.MixedData.mergeCheck540 line 296
  95. theorem OAI.MUB6.Certificate.MixedData.mergedZero540 line 298
  96. def OAI.MUB6.Certificate.MixedData.merged541 line 303
  97. theorem OAI.MUB6.Certificate.MixedData.mergeCheck541 line 305
  98. theorem OAI.MUB6.Certificate.MixedData.mergedZero541 line 307
  99. def OAI.MUB6.Certificate.MixedData.merged542 line 313
  100. theorem OAI.MUB6.Certificate.MixedData.mergeCheck542 line 315
  101. theorem OAI.MUB6.Certificate.MixedData.mergedZero542 line 317
  102. def OAI.MUB6.Certificate.MixedData.merged543 line 323
  103. theorem OAI.MUB6.Certificate.MixedData.mergeCheck543 line 325
  104. theorem OAI.MUB6.Certificate.MixedData.mergedZero543 line 327