OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionMergeData3.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge96 line 12
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge96 line 14
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge96Check line 16
  4. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge97 line 18
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge97 line 20
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge97Check line 22
  7. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge98 line 24
  8. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge98 line 26
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge98Check line 28
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge99 line 30
  11. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge99 line 32
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge99Check line 34
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge100 line 36
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge100 line 38
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge100Check line 40
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge101 line 42
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge101 line 44
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge101Check line 46
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge102 line 48
  20. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge102 line 50
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge102Check line 52
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge103 line 54
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge103 line 56
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge103Check line 58
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge104 line 60
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge104 line 62
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge104Check line 64
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge105 line 66
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge105 line 68
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge105Check line 70
  31. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge106 line 72
  32. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge106 line 74
  33. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge106Check line 76
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge107 line 78
  35. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge107 line 80
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge107Check line 82
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge108 line 84
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge108 line 86
  39. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge108Check line 88
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge109 line 90
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge109 line 92
  42. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge109Check line 94
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge110 line 96
  44. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge110 line 98
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge110Check line 100
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge111 line 102
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge111 line 104
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge111Check line 106
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge112 line 108
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge112 line 110
  51. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge112Check line 112
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge113 line 114
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge113 line 116
  54. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge113Check line 118
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge114 line 120
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge114 line 122
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge114Check line 124
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge115 line 126
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge115 line 128
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge115Check line 130
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge116 line 132
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge116 line 134
  63. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge116Check line 136
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge117 line 138
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge117 line 140
  66. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge117Check line 142
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge118 line 144
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge118 line 146
  69. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge118Check line 148
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge119 line 150
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge119 line 152
  72. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge119Check line 154
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge120 line 156
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge120 line 158
  75. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge120Check line 160
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge121 line 162
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge121 line 164
  78. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge121Check line 166
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge122 line 168
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge122 line 170
  81. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge122Check line 172
  82. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge123 line 174
  83. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge123 line 176
  84. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge123Check line 178
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge124 line 180
  86. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge124 line 182
  87. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge124Check line 184
  88. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge125 line 186
  89. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge125 line 188
  90. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge125Check line 190
  91. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge126 line 192
  92. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge126 line 194
  93. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge126Check line 196
  94. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge127 line 198
  95. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge127 line 200
  96. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge127Check line 202