OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionMergeData15.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge480 line 11
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge480 line 13
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge480Check line 15
  4. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge481 line 17
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge481 line 19
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge481Check line 21
  7. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge482 line 23
  8. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge482 line 25
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge482Check line 27
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge483 line 29
  11. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge483 line 31
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge483Check line 33
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge484 line 35
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge484 line 37
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge484Check line 39
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge485 line 41
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge485 line 43
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge485Check line 45
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge486 line 47
  20. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge486 line 49
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge486Check line 51
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge487 line 53
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge487 line 55
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge487Check line 57
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge488 line 59
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge488 line 61
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge488Check line 63
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge489 line 65
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge489 line 67
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge489Check line 69
  31. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge490 line 71
  32. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge490 line 73
  33. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge490Check line 75
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge491 line 77
  35. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge491 line 79
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge491Check line 81
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge492 line 83
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge492 line 85
  39. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge492Check line 87
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge493 line 89
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge493 line 91
  42. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge493Check line 93
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge494 line 95
  44. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge494 line 97
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge494Check line 99
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge495 line 101
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge495 line 103
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge495Check line 105
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge496 line 107
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge496 line 109
  51. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge496Check line 111
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge497 line 113
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge497 line 115
  54. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge497Check line 117
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge498 line 119
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge498 line 121
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge498Check line 123
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge499 line 125
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge499 line 127
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge499Check line 129
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge500 line 131
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge500 line 133
  63. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge500Check line 135
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge501 line 137
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge501 line 139
  66. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge501Check line 141
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge502 line 143
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge502 line 145
  69. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge502Check line 147
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge503 line 149
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge503 line 151
  72. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge503Check line 153
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge504 line 155
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge504 line 157
  75. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge504Check line 159
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge505 line 161
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge505 line 163
  78. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge505Check line 165
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge506 line 167
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge506 line 169
  81. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge506Check line 171
  82. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge507 line 173
  83. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge507 line 175
  84. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge507Check line 177
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge508 line 179
  86. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge508 line 181
  87. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge508Check line 183
  88. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge509 line 185
  89. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge509 line 187
  90. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge509Check line 189
  91. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge510 line 191
  92. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge510 line 193
  93. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge510Check line 195
  94. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge511 line 197
  95. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge511 line 199
  96. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge511Check line 201