OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionMergeData44.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1408 line 14
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1408 line 16
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1408Check line 18
  4. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1409 line 20
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1409 line 22
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1409Check line 24
  7. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1410 line 26
  8. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1410 line 28
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1410Check line 30
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1411 line 32
  11. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1411 line 34
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1411Check line 36
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1412 line 38
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1412 line 40
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1412Check line 42
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1413 line 44
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1413 line 46
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1413Check line 48
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1414 line 50
  20. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1414 line 52
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1414Check line 54
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1415 line 56
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1415 line 58
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1415Check line 60
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1416 line 62
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1416 line 64
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1416Check line 66
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1417 line 68
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1417 line 70
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1417Check line 72
  31. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1418 line 74
  32. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1418 line 76
  33. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1418Check line 78
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1419 line 80
  35. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1419 line 82
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1419Check line 84
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1420 line 86
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1420 line 88
  39. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1420Check line 90
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1421 line 92
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1421 line 94
  42. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1421Check line 96
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1422 line 98
  44. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1422 line 100
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1422Check line 102
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1423 line 104
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1423 line 106
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1423Check line 108
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1424 line 110
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1424 line 112
  51. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1424Check line 114
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1425 line 116
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1425 line 118
  54. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1425Check line 120
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1426 line 122
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1426 line 124
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1426Check line 126
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1427 line 128
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1427 line 130
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1427Check line 132
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1428 line 134
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1428 line 136
  63. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1428Check line 138
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1429 line 140
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1429 line 142
  66. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1429Check line 144
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1430 line 146
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1430 line 148
  69. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1430Check line 150
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1431 line 152
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1431 line 154
  72. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1431Check line 156
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1432 line 158
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1432 line 160
  75. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1432Check line 162
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1433 line 164
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1433 line 166
  78. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1433Check line 168
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1434 line 170
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1434 line 172
  81. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1434Check line 174
  82. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1435 line 176
  83. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1435 line 178
  84. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1435Check line 180
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1436part0 line 182
  86. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1436part1 line 184
  87. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1436part2 line 186
  88. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1436part3 line 188
  89. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1436part4 line 190
  90. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1436part5 line 192
  91. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1436part6 line 194
  92. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1436 line 196
  93. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1436 line 198
  94. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1436Check line 200
  95. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1437 line 202
  96. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1437 line 204
  97. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1437Check line 206
  98. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1438 line 208
  99. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1438 line 210
  100. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1438Check line 212
  101. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1439 line 214
  102. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1439 line 216
  103. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1439Check line 218