OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionMergeData14.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge448 line 14
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge448 line 16
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge448Check line 18
  4. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge449 line 20
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge449 line 22
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge449Check line 24
  7. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge450 line 26
  8. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge450 line 28
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge450Check line 30
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge451 line 32
  11. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge451 line 34
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge451Check line 36
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge452 line 38
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge452 line 40
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge452Check line 42
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge453 line 44
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge453 line 46
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge453Check line 48
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge454 line 50
  20. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge454 line 52
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge454Check line 54
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge455 line 56
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge455 line 58
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge455Check line 60
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge456 line 62
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge456 line 64
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge456Check line 66
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge457 line 68
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge457 line 70
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge457Check line 72
  31. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge458 line 74
  32. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge458 line 76
  33. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge458Check line 78
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge459 line 80
  35. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge459 line 82
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge459Check line 84
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge460 line 86
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge460 line 88
  39. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge460Check line 90
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge461 line 92
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge461 line 94
  42. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge461Check line 96
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge462 line 98
  44. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge462 line 100
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge462Check line 102
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge463 line 104
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge463 line 106
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge463Check line 108
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge464 line 110
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge464 line 112
  51. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge464Check line 114
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge465 line 116
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge465 line 118
  54. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge465Check line 120
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge466 line 122
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge466 line 124
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge466Check line 126
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge467 line 128
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge467 line 130
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge467Check line 132
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge468 line 134
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge468 line 136
  63. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge468Check line 138
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge469 line 140
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge469 line 142
  66. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge469Check line 144
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge470 line 146
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge470 line 148
  69. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge470Check line 150
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge471 line 152
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge471 line 154
  72. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge471Check line 156
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge472 line 158
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge472 line 160
  75. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge472Check line 162
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge473 line 164
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge473 line 166
  78. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge473Check line 168
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge474 line 170
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge474 line 172
  81. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge474Check line 174
  82. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge475 line 176
  83. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge475 line 178
  84. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge475Check line 180
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge476 line 182
  86. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge476 line 184
  87. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge476Check line 186
  88. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge477 line 188
  89. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge477 line 190
  90. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge477Check line 192
  91. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge478 line 194
  92. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge478 line 196
  93. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge478Check line 198
  94. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge479 line 200
  95. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge479 line 202
  96. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge479Check line 204