OAI/Analysis/MutuallyUnbiased/MixedMerge/Block64.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged2048 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2048 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero2048 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged2049 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2049 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero2049 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged2050 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2050 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero2050 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged2051 line 37
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2051 line 39
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero2051 line 41
  13. def OAI.MUB6.Certificate.MixedData.merged2052 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2052 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero2052 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged2053 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2053 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero2053 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged2054 line 66
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2054 line 68
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero2054 line 70
  22. def OAI.MUB6.Certificate.MixedData.merged2055 line 75
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2055 line 77
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero2055 line 79
  25. def OAI.MUB6.Certificate.MixedData.merged2056 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2056 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero2056 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged2057 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2057 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero2057 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged2058 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2058 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero2058 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged2059 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2059 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero2059 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged2060 line 124
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2060 line 126
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero2060 line 128
  40. def OAI.MUB6.Certificate.MixedData.merged2061 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2061 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero2061 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged2062 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2062 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero2062 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged2063 line 152
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2063 line 154
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero2063 line 156
  49. def OAI.MUB6.Certificate.MixedData.merged2064 line 161
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2064 line 163
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero2064 line 165
  52. def OAI.MUB6.Certificate.MixedData.merged2065 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2065 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero2065 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged2066 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2066 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero2066 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged2067 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2067 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero2067 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged2068 line 200
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2068 line 202
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero2068 line 204
  64. def OAI.MUB6.Certificate.MixedData.merged2069 line 209
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2069 line 211
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero2069 line 213
  67. def OAI.MUB6.Certificate.MixedData.merged2070 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2070 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero2070 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged2071 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2071 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero2071 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged2072 line 238
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2072 line 240
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero2072 line 242
  76. def OAI.MUB6.Certificate.MixedData.merged2073 line 247
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2073 line 249
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero2073 line 251
  79. def OAI.MUB6.Certificate.MixedData.merged2074 line 257
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2074 line 259
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero2074 line 261
  82. def OAI.MUB6.Certificate.MixedData.merged2075 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2075 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero2075 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged2076 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2076 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero2076 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged2077part0 line 287
  89. def OAI.MUB6.Certificate.MixedData.merged2077part1 line 289
  90. def OAI.MUB6.Certificate.MixedData.merged2077part2 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged2077part3 line 293
  92. def OAI.MUB6.Certificate.MixedData.merged2077part4 line 295
  93. def OAI.MUB6.Certificate.MixedData.merged2077part5 line 297
  94. def OAI.MUB6.Certificate.MixedData.merged2077part6 line 299
  95. def OAI.MUB6.Certificate.MixedData.merged2077part7 line 301
  96. def OAI.MUB6.Certificate.MixedData.merged2077 line 303
  97. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2077 line 305
  98. theorem OAI.MUB6.Certificate.MixedData.mergedZero2077 line 307
  99. def OAI.MUB6.Certificate.MixedData.merged2078 line 313
  100. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2078 line 315
  101. theorem OAI.MUB6.Certificate.MixedData.mergedZero2078 line 317
  102. def OAI.MUB6.Certificate.MixedData.merged2079 line 322
  103. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2079 line 324
  104. theorem OAI.MUB6.Certificate.MixedData.mergedZero2079 line 326