OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionMergeData0.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge0 line 10
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge0 line 12
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge0Check line 14
  4. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1 line 16
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1 line 18
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1Check line 20
  7. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge2 line 22
  8. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge2 line 24
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge2Check line 26
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge3 line 28
  11. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge3 line 30
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge3Check line 32
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge4 line 34
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge4 line 36
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge4Check line 38
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge5 line 40
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge5 line 42
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge5Check line 44
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge6 line 46
  20. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge6 line 48
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge6Check line 50
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge7 line 52
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge7 line 54
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge7Check line 56
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge8 line 58
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge8 line 60
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge8Check line 62
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge9 line 64
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge9 line 66
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge9Check line 68
  31. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge10 line 70
  32. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge10 line 72
  33. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge10Check line 74
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge11 line 76
  35. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge11 line 78
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge11Check line 80
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge12 line 82
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge12 line 84
  39. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge12Check line 86
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge13 line 88
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge13 line 90
  42. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge13Check line 92
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge14 line 94
  44. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge14 line 96
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge14Check line 98
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge15 line 100
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge15 line 102
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge15Check line 104
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge16 line 106
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge16 line 108
  51. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge16Check line 110
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge17 line 112
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge17 line 114
  54. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge17Check line 116
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge18 line 118
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge18 line 120
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge18Check line 122
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge19 line 124
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge19 line 126
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge19Check line 128
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge20 line 130
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge20 line 132
  63. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge20Check line 134
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge21 line 136
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge21 line 138
  66. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge21Check line 140
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge22 line 142
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge22 line 144
  69. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge22Check line 146
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge23 line 148
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge23 line 150
  72. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge23Check line 152
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge24 line 154
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge24 line 156
  75. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge24Check line 158
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge25 line 160
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge25 line 162
  78. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge25Check line 164
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge26 line 166
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge26 line 168
  81. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge26Check line 170
  82. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge27 line 172
  83. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge27 line 174
  84. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge27Check line 176
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge28 line 178
  86. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge28 line 180
  87. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge28Check line 182
  88. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge29 line 184
  89. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge29 line 186
  90. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge29Check line 188
  91. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge30 line 190
  92. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge30 line 192
  93. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge30Check line 194
  94. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge31 line 196
  95. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge31 line 198
  96. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge31Check line 200