OAI/Analysis/MutuallyUnbiased/MixedMerge/Block74.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged2368 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2368 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero2368 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged2369 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2369 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero2369 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged2370 line 29
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2370 line 31
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero2370 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged2371 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2371 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero2371 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged2372 line 47
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2372 line 49
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero2372 line 51
  16. def OAI.MUB6.Certificate.MixedData.merged2373 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2373 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero2373 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged2374 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2374 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero2374 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged2375 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2375 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero2375 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged2376 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2376 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero2376 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged2377 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2377 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero2377 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged2378 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2378 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero2378 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged2379 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2379 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero2379 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged2380 line 125
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2380 line 127
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero2380 line 129
  40. def OAI.MUB6.Certificate.MixedData.merged2381 line 135
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2381 line 137
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero2381 line 139
  43. def OAI.MUB6.Certificate.MixedData.merged2382 line 144
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2382 line 146
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero2382 line 148
  46. def OAI.MUB6.Certificate.MixedData.merged2383 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2383 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero2383 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged2384 line 163
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2384 line 165
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero2384 line 167
  52. def OAI.MUB6.Certificate.MixedData.merged2385 line 172
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2385 line 174
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero2385 line 176
  55. def OAI.MUB6.Certificate.MixedData.merged2386 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2386 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero2386 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged2387 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2387 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero2387 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged2388 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2388 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero2388 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged2389 line 211
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2389 line 213
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero2389 line 215
  67. def OAI.MUB6.Certificate.MixedData.merged2390 line 220
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2390 line 222
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero2390 line 224
  70. def OAI.MUB6.Certificate.MixedData.merged2391 line 229
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2391 line 231
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero2391 line 233
  73. def OAI.MUB6.Certificate.MixedData.merged2392 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2392 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero2392 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged2393 line 249
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2393 line 251
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero2393 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged2394 line 258
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2394 line 260
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero2394 line 262
  82. def OAI.MUB6.Certificate.MixedData.merged2395 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2395 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero2395 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged2396 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2396 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero2396 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged2397 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2397 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero2397 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged2398 line 297
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2398 line 299
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero2398 line 301
  94. def OAI.MUB6.Certificate.MixedData.merged2399 line 307
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck2399 line 309
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero2399 line 311