OAI/Analysis/MutuallyUnbiased/MixedMerge/Block1.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged32 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck32 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero32 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged33 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck33 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero33 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged34 line 29
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck34 line 31
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero34 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged35 line 39
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck35 line 41
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero35 line 43
  13. def OAI.MUB6.Certificate.MixedData.merged36 line 49
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck36 line 51
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero36 line 53
  16. def OAI.MUB6.Certificate.MixedData.merged37 line 58
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck37 line 60
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero37 line 62
  19. def OAI.MUB6.Certificate.MixedData.merged38 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck38 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero38 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged39 line 77
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck39 line 79
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero39 line 81
  25. def OAI.MUB6.Certificate.MixedData.merged40 line 86
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck40 line 88
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero40 line 90
  28. def OAI.MUB6.Certificate.MixedData.merged41 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck41 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero41 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged42 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck42 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero42 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged43 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck43 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero43 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged44 line 125
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck44 line 127
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero44 line 129
  40. def OAI.MUB6.Certificate.MixedData.merged45 line 134
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck45 line 136
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero45 line 138
  43. def OAI.MUB6.Certificate.MixedData.merged46 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck46 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero46 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged47 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck47 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero47 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged48 line 163
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck48 line 165
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero48 line 167
  52. def OAI.MUB6.Certificate.MixedData.merged49 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck49 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero49 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged50 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck50 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero50 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged51 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck51 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero51 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged52 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck52 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero52 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged53 line 211
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck53 line 213
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero53 line 215
  67. def OAI.MUB6.Certificate.MixedData.merged54 line 221
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck54 line 223
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero54 line 225
  70. def OAI.MUB6.Certificate.MixedData.merged55 line 230
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck55 line 232
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero55 line 234
  73. def OAI.MUB6.Certificate.MixedData.merged56 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck56 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero56 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged57 line 249
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck57 line 251
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero57 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged58 line 258
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck58 line 260
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero58 line 262
  82. def OAI.MUB6.Certificate.MixedData.merged59 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck59 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero59 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged60 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck60 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero60 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged61 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck61 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero61 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged62 line 297
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck62 line 299
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero62 line 301
  94. def OAI.MUB6.Certificate.MixedData.merged63 line 306
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck63 line 308
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero63 line 310