OAI/Analysis/MutuallyUnbiased/MixedMerge/Block42.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1344 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1344 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1344 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1345 line 18
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1345 line 20
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1345 line 22
  7. def OAI.MUB6.Certificate.MixedData.merged1346 line 28
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1346 line 30
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1346 line 32
  10. def OAI.MUB6.Certificate.MixedData.merged1347 line 38
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1347 line 40
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1347 line 42
  13. def OAI.MUB6.Certificate.MixedData.merged1348 line 48
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1348 line 50
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1348 line 52
  16. def OAI.MUB6.Certificate.MixedData.merged1349 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1349 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1349 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged1350 line 66
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1350 line 68
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1350 line 70
  22. def OAI.MUB6.Certificate.MixedData.merged1351 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1351 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1351 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged1352 line 86
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1352 line 88
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1352 line 90
  28. def OAI.MUB6.Certificate.MixedData.merged1353 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1353 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1353 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged1354 line 104
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1354 line 106
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1354 line 108
  34. def OAI.MUB6.Certificate.MixedData.merged1355 line 114
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1355 line 116
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1355 line 118
  37. def OAI.MUB6.Certificate.MixedData.merged1356 line 124
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1356 line 126
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1356 line 128
  40. def OAI.MUB6.Certificate.MixedData.merged1357 line 134
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1357 line 136
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1357 line 138
  43. def OAI.MUB6.Certificate.MixedData.merged1358 line 144
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1358 line 146
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1358 line 148
  46. def OAI.MUB6.Certificate.MixedData.merged1359 line 154
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1359 line 156
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1359 line 158
  49. def OAI.MUB6.Certificate.MixedData.merged1360part0 line 164
  50. def OAI.MUB6.Certificate.MixedData.merged1360part1 line 166
  51. def OAI.MUB6.Certificate.MixedData.merged1360part2 line 168
  52. def OAI.MUB6.Certificate.MixedData.merged1360part3 line 170
  53. def OAI.MUB6.Certificate.MixedData.merged1360part4 line 172
  54. def OAI.MUB6.Certificate.MixedData.merged1360part5 line 174
  55. def OAI.MUB6.Certificate.MixedData.merged1360part6 line 176
  56. def OAI.MUB6.Certificate.MixedData.merged1360part7 line 178
  57. def OAI.MUB6.Certificate.MixedData.merged1360part8 line 180
  58. def OAI.MUB6.Certificate.MixedData.merged1360part9 line 182
  59. def OAI.MUB6.Certificate.MixedData.merged1360 line 184
  60. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1360 line 186
  61. theorem OAI.MUB6.Certificate.MixedData.mergedZero1360 line 188
  62. def OAI.MUB6.Certificate.MixedData.merged1361 line 194
  63. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1361 line 196
  64. theorem OAI.MUB6.Certificate.MixedData.mergedZero1361 line 198
  65. def OAI.MUB6.Certificate.MixedData.merged1362 line 203
  66. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1362 line 205
  67. theorem OAI.MUB6.Certificate.MixedData.mergedZero1362 line 207
  68. def OAI.MUB6.Certificate.MixedData.merged1363 line 212
  69. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1363 line 214
  70. theorem OAI.MUB6.Certificate.MixedData.mergedZero1363 line 216
  71. def OAI.MUB6.Certificate.MixedData.merged1364 line 222
  72. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1364 line 224
  73. theorem OAI.MUB6.Certificate.MixedData.mergedZero1364 line 226
  74. def OAI.MUB6.Certificate.MixedData.merged1365 line 231
  75. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1365 line 233
  76. theorem OAI.MUB6.Certificate.MixedData.mergedZero1365 line 235
  77. def OAI.MUB6.Certificate.MixedData.merged1366 line 240
  78. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1366 line 242
  79. theorem OAI.MUB6.Certificate.MixedData.mergedZero1366 line 244
  80. def OAI.MUB6.Certificate.MixedData.merged1367 line 250
  81. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1367 line 252
  82. theorem OAI.MUB6.Certificate.MixedData.mergedZero1367 line 254
  83. def OAI.MUB6.Certificate.MixedData.merged1368 line 260
  84. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1368 line 262
  85. theorem OAI.MUB6.Certificate.MixedData.mergedZero1368 line 264
  86. def OAI.MUB6.Certificate.MixedData.merged1369 line 270
  87. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1369 line 272
  88. theorem OAI.MUB6.Certificate.MixedData.mergedZero1369 line 274
  89. def OAI.MUB6.Certificate.MixedData.merged1370 line 279
  90. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1370 line 281
  91. theorem OAI.MUB6.Certificate.MixedData.mergedZero1370 line 283
  92. def OAI.MUB6.Certificate.MixedData.merged1371 line 288
  93. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1371 line 290
  94. theorem OAI.MUB6.Certificate.MixedData.mergedZero1371 line 292
  95. def OAI.MUB6.Certificate.MixedData.merged1372 line 298
  96. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1372 line 300
  97. theorem OAI.MUB6.Certificate.MixedData.mergedZero1372 line 302
  98. def OAI.MUB6.Certificate.MixedData.merged1373 line 308
  99. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1373 line 310
  100. theorem OAI.MUB6.Certificate.MixedData.mergedZero1373 line 312
  101. def OAI.MUB6.Certificate.MixedData.merged1374 line 317
  102. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1374 line 319
  103. theorem OAI.MUB6.Certificate.MixedData.mergedZero1374 line 321
  104. def OAI.MUB6.Certificate.MixedData.merged1375 line 326
  105. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1375 line 328
  106. theorem OAI.MUB6.Certificate.MixedData.mergedZero1375 line 330