OAI/Analysis/MutuallyUnbiased/MixedMerge/Block65.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged2080 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2080 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero2080 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged2081 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2081 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero2081 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged2082 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2082 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero2082 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged2083 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2083 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero2083 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged2084 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2084 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero2084 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged2085 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2085 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero2085 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged2086 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2086 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero2086 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged2087 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2087 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero2087 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged2088 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2088 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero2088 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged2089 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2089 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero2089 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged2090 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2090 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero2090 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged2091 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2091 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero2091 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged2092 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2092 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero2092 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged2093 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2093 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero2093 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged2094 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2094 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero2094 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged2095 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2095 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero2095 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged2096 line 163
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2096 line 165
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero2096 line 167
  52. def OAI.MUB6.Certificate.MixedData.merged2097 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2097 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero2097 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged2098 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2098 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero2098 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged2099 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2099 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero2099 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged2100 line 200
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2100 line 202
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero2100 line 204
  64. def OAI.MUB6.Certificate.MixedData.merged2101 line 209
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2101 line 211
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero2101 line 213
  67. def OAI.MUB6.Certificate.MixedData.merged2102 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2102 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero2102 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged2103 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2103 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero2103 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged2104 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2104 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero2104 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged2105 line 248
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2105 line 250
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero2105 line 252
  79. def OAI.MUB6.Certificate.MixedData.merged2106 line 257
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2106 line 259
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero2106 line 261
  82. def OAI.MUB6.Certificate.MixedData.merged2107 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2107 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero2107 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged2108 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2108 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero2108 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged2109 line 286
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2109 line 288
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero2109 line 290
  91. def OAI.MUB6.Certificate.MixedData.merged2110 line 295
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2110 line 297
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero2110 line 299
  94. def OAI.MUB6.Certificate.MixedData.merged2111 line 305
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2111 line 307
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero2111 line 309