OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionMergeData13.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge416 line 10
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge416 line 12
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge416Check line 14
  4. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge417 line 16
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge417 line 18
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge417Check line 20
  7. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge418 line 22
  8. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge418 line 24
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge418Check line 26
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge419 line 28
  11. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge419 line 30
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge419Check line 32
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge420 line 34
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge420 line 36
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge420Check line 38
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge421 line 40
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge421 line 42
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge421Check line 44
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge422 line 46
  20. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge422 line 48
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge422Check line 50
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge423 line 52
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge423 line 54
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge423Check line 56
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge424 line 58
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge424 line 60
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge424Check line 62
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge425 line 64
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge425 line 66
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge425Check line 68
  31. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge426 line 70
  32. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge426 line 72
  33. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge426Check line 74
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge427 line 76
  35. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge427 line 78
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge427Check line 80
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge428 line 82
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge428 line 84
  39. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge428Check line 86
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge429 line 88
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge429 line 90
  42. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge429Check line 92
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge430 line 94
  44. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge430 line 96
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge430Check line 98
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge431 line 100
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge431 line 102
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge431Check line 104
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge432 line 106
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge432 line 108
  51. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge432Check line 110
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge433 line 112
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge433 line 114
  54. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge433Check line 116
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge434 line 118
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge434 line 120
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge434Check line 122
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge435 line 124
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge435 line 126
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge435Check line 128
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge436 line 130
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge436 line 132
  63. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge436Check line 134
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge437 line 136
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge437 line 138
  66. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge437Check line 140
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge438 line 142
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge438 line 144
  69. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge438Check line 146
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge439 line 148
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge439 line 150
  72. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge439Check line 152
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge440 line 154
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge440 line 156
  75. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge440Check line 158
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge441 line 160
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge441 line 162
  78. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge441Check line 164
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge442 line 166
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge442 line 168
  81. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge442Check line 170
  82. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge443 line 172
  83. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge443 line 174
  84. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge443Check line 176
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge444 line 178
  86. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge444 line 180
  87. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge444Check line 182
  88. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge445 line 184
  89. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge445 line 186
  90. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge445Check line 188
  91. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge446 line 190
  92. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge446 line 192
  93. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge446Check line 194
  94. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge447 line 196
  95. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge447 line 198
  96. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge447Check line 200