OAI/Analysis/MutuallyUnbiased/MixedMerge/Block72.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged2304 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2304 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero2304 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged2305 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2305 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero2305 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged2306 line 29
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2306 line 31
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero2306 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged2307 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2307 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero2307 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged2308 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2308 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero2308 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged2309 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2309 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero2309 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged2310 line 66
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2310 line 68
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero2310 line 70
  22. def OAI.MUB6.Certificate.MixedData.merged2311 line 75
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2311 line 77
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero2311 line 79
  25. def OAI.MUB6.Certificate.MixedData.merged2312 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2312 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero2312 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged2313 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2313 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero2313 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged2314 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2314 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero2314 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged2315 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2315 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero2315 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged2316 line 123
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2316 line 125
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero2316 line 127
  40. def OAI.MUB6.Certificate.MixedData.merged2317 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2317 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero2317 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged2318 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2318 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero2318 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged2319 line 152
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2319 line 154
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero2319 line 156
  49. def OAI.MUB6.Certificate.MixedData.merged2320 line 161
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2320 line 163
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero2320 line 165
  52. def OAI.MUB6.Certificate.MixedData.merged2321 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2321 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero2321 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged2322 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2322 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero2322 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged2323 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2323 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero2323 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged2324 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2324 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero2324 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged2325 line 210
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2325 line 212
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero2325 line 214
  67. def OAI.MUB6.Certificate.MixedData.merged2326 line 219
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2326 line 221
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero2326 line 223
  70. def OAI.MUB6.Certificate.MixedData.merged2327 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2327 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero2327 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged2328 line 238
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2328 line 240
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero2328 line 242
  76. def OAI.MUB6.Certificate.MixedData.merged2329 line 247
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2329 line 249
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero2329 line 251
  79. def OAI.MUB6.Certificate.MixedData.merged2330 line 257
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2330 line 259
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero2330 line 261
  82. def OAI.MUB6.Certificate.MixedData.merged2331 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2331 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero2331 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged2332 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2332 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero2332 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged2333 line 286
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2333 line 288
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero2333 line 290
  91. def OAI.MUB6.Certificate.MixedData.merged2334 line 295
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2334 line 297
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero2334 line 299
  94. def OAI.MUB6.Certificate.MixedData.merged2335 line 305
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2335 line 307
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero2335 line 309