OAI/Analysis/MutuallyUnbiased/MixedMerge/Block43.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedData.merged1376 line 9
  2. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1376 line 11
  3. theorem OAI.MUB6.Certificate.MixedData.mergedZero1376 line 13
  4. def OAI.MUB6.Certificate.MixedData.merged1377 line 19
  5. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1377 line 21
  6. theorem OAI.MUB6.Certificate.MixedData.mergedZero1377 line 23
  7. def OAI.MUB6.Certificate.MixedData.merged1378 line 29
  8. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1378 line 31
  9. theorem OAI.MUB6.Certificate.MixedData.mergedZero1378 line 33
  10. def OAI.MUB6.Certificate.MixedData.merged1379 line 39
  11. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1379 line 41
  12. theorem OAI.MUB6.Certificate.MixedData.mergedZero1379 line 43
  13. def OAI.MUB6.Certificate.MixedData.merged1380 line 48
  14. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1380 line 50
  15. theorem OAI.MUB6.Certificate.MixedData.mergedZero1380 line 52
  16. def OAI.MUB6.Certificate.MixedData.merged1381 line 57
  17. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1381 line 59
  18. theorem OAI.MUB6.Certificate.MixedData.mergedZero1381 line 61
  19. def OAI.MUB6.Certificate.MixedData.merged1382 line 67
  20. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1382 line 69
  21. theorem OAI.MUB6.Certificate.MixedData.mergedZero1382 line 71
  22. def OAI.MUB6.Certificate.MixedData.merged1383 line 76
  23. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1383 line 78
  24. theorem OAI.MUB6.Certificate.MixedData.mergedZero1383 line 80
  25. def OAI.MUB6.Certificate.MixedData.merged1384 line 85
  26. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1384 line 87
  27. theorem OAI.MUB6.Certificate.MixedData.mergedZero1384 line 89
  28. def OAI.MUB6.Certificate.MixedData.merged1385 line 95
  29. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1385 line 97
  30. theorem OAI.MUB6.Certificate.MixedData.mergedZero1385 line 99
  31. def OAI.MUB6.Certificate.MixedData.merged1386 line 105
  32. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1386 line 107
  33. theorem OAI.MUB6.Certificate.MixedData.mergedZero1386 line 109
  34. def OAI.MUB6.Certificate.MixedData.merged1387 line 115
  35. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1387 line 117
  36. theorem OAI.MUB6.Certificate.MixedData.mergedZero1387 line 119
  37. def OAI.MUB6.Certificate.MixedData.merged1388 line 124
  38. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1388 line 126
  39. theorem OAI.MUB6.Certificate.MixedData.mergedZero1388 line 128
  40. def OAI.MUB6.Certificate.MixedData.merged1389 line 133
  41. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1389 line 135
  42. theorem OAI.MUB6.Certificate.MixedData.mergedZero1389 line 137
  43. def OAI.MUB6.Certificate.MixedData.merged1390 line 143
  44. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1390 line 145
  45. theorem OAI.MUB6.Certificate.MixedData.mergedZero1390 line 147
  46. def OAI.MUB6.Certificate.MixedData.merged1391 line 153
  47. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1391 line 155
  48. theorem OAI.MUB6.Certificate.MixedData.mergedZero1391 line 157
  49. def OAI.MUB6.Certificate.MixedData.merged1392 line 162
  50. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1392 line 164
  51. theorem OAI.MUB6.Certificate.MixedData.mergedZero1392 line 166
  52. def OAI.MUB6.Certificate.MixedData.merged1393 line 171
  53. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1393 line 173
  54. theorem OAI.MUB6.Certificate.MixedData.mergedZero1393 line 175
  55. def OAI.MUB6.Certificate.MixedData.merged1394 line 181
  56. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1394 line 183
  57. theorem OAI.MUB6.Certificate.MixedData.mergedZero1394 line 185
  58. def OAI.MUB6.Certificate.MixedData.merged1395 line 191
  59. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1395 line 193
  60. theorem OAI.MUB6.Certificate.MixedData.mergedZero1395 line 195
  61. def OAI.MUB6.Certificate.MixedData.merged1396 line 201
  62. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1396 line 203
  63. theorem OAI.MUB6.Certificate.MixedData.mergedZero1396 line 205
  64. def OAI.MUB6.Certificate.MixedData.merged1397 line 211
  65. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1397 line 213
  66. theorem OAI.MUB6.Certificate.MixedData.mergedZero1397 line 215
  67. def OAI.MUB6.Certificate.MixedData.merged1398 line 221
  68. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1398 line 223
  69. theorem OAI.MUB6.Certificate.MixedData.mergedZero1398 line 225
  70. def OAI.MUB6.Certificate.MixedData.merged1399 line 230
  71. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1399 line 232
  72. theorem OAI.MUB6.Certificate.MixedData.mergedZero1399 line 234
  73. def OAI.MUB6.Certificate.MixedData.merged1400 line 239
  74. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1400 line 241
  75. theorem OAI.MUB6.Certificate.MixedData.mergedZero1400 line 243
  76. def OAI.MUB6.Certificate.MixedData.merged1401 line 249
  77. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1401 line 251
  78. theorem OAI.MUB6.Certificate.MixedData.mergedZero1401 line 253
  79. def OAI.MUB6.Certificate.MixedData.merged1402 line 258
  80. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1402 line 260
  81. theorem OAI.MUB6.Certificate.MixedData.mergedZero1402 line 262
  82. def OAI.MUB6.Certificate.MixedData.merged1403 line 267
  83. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1403 line 269
  84. theorem OAI.MUB6.Certificate.MixedData.mergedZero1403 line 271
  85. def OAI.MUB6.Certificate.MixedData.merged1404 line 277
  86. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1404 line 279
  87. theorem OAI.MUB6.Certificate.MixedData.mergedZero1404 line 281
  88. def OAI.MUB6.Certificate.MixedData.merged1405 line 287
  89. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1405 line 289
  90. theorem OAI.MUB6.Certificate.MixedData.mergedZero1405 line 291
  91. def OAI.MUB6.Certificate.MixedData.merged1406 line 297
  92. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1406 line 299
  93. theorem OAI.MUB6.Certificate.MixedData.mergedZero1406 line 301
  94. def OAI.MUB6.Certificate.MixedData.merged1407 line 306
  95. theorem OAI.MUB6.Certificate.MixedData.mergeCheck1407 line 308
  96. theorem OAI.MUB6.Certificate.MixedData.mergedZero1407 line 310