OAI/Analysis/MutuallyUnbiased/MixedMerge/Block15.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged480 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck480 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero480 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged481 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck481 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero481 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged482 line 29
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck482 line 31
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero482 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged483 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck483 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero483 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged484 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck484 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero484 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged485 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck485 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero485 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged486 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck486 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero486 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged487 line 77
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck487 line 79
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero487 line 81
  25. def OAI.MUB6.Certificate.MixedData.merged488 line 87
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck488 line 89
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero488 line 91
  28. def OAI.MUB6.Certificate.MixedData.merged489 line 97
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck489 line 99
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero489 line 101
  31. def OAI.MUB6.Certificate.MixedData.merged490 line 106
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck490 line 108
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero490 line 110
  34. def OAI.MUB6.Certificate.MixedData.merged491 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck491 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero491 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged492 line 125
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck492 line 127
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero492 line 129
  40. def OAI.MUB6.Certificate.MixedData.merged493 line 134
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck493 line 136
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero493 line 138
  43. def OAI.MUB6.Certificate.MixedData.merged494 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck494 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero494 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged495 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck495 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero495 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged496 line 163
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck496 line 165
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero496 line 167
  52. def OAI.MUB6.Certificate.MixedData.merged497 line 173
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck497 line 175
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero497 line 177
  55. def OAI.MUB6.Certificate.MixedData.merged498 line 182
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck498 line 184
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero498 line 186
  58. def OAI.MUB6.Certificate.MixedData.merged499 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck499 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero499 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged500 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck500 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero500 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged501 line 211
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck501 line 213
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero501 line 215
  67. def OAI.MUB6.Certificate.MixedData.merged502 line 220
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck502 line 222
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero502 line 224
  70. def OAI.MUB6.Certificate.MixedData.merged503 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck503 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero503 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged504 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck504 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero504 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged505 line 249
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck505 line 251
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero505 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged506 line 259
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck506 line 261
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero506 line 263
  82. def OAI.MUB6.Certificate.MixedData.merged507 line 269
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck507 line 271
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero507 line 273
  85. def OAI.MUB6.Certificate.MixedData.merged508 line 278
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck508 line 280
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero508 line 282
  88. def OAI.MUB6.Certificate.MixedData.merged509 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck509 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero509 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged510 line 297
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck510 line 299
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero510 line 301
  94. def OAI.MUB6.Certificate.MixedData.merged511 line 306
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck511 line 308
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero511 line 310