OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionMergeData56.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1792 line 12
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1792 line 14
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1792Check line 16
  4. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1793 line 18
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1793 line 20
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1793Check line 22
  7. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1794 line 24
  8. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1794 line 26
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1794Check line 28
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1795 line 30
  11. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1795 line 32
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1795Check line 34
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1796 line 36
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1796 line 38
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1796Check line 40
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1797 line 42
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1797 line 44
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1797Check line 46
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1798 line 48
  20. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1798 line 50
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1798Check line 52
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1799 line 54
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1799 line 56
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1799Check line 58
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1800 line 60
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1800 line 62
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1800Check line 64
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1801 line 66
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1801 line 68
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1801Check line 70
  31. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1802 line 72
  32. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1802 line 74
  33. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1802Check line 76
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1803 line 78
  35. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1803 line 80
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1803Check line 82
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1804 line 84
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1804 line 86
  39. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1804Check line 88
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1805 line 90
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1805 line 92
  42. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1805Check line 94
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1806 line 96
  44. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1806 line 98
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1806Check line 100
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1807 line 102
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1807 line 104
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1807Check line 106
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1808 line 108
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1808 line 110
  51. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1808Check line 112
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1809 line 114
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1809 line 116
  54. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1809Check line 118
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1810 line 120
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1810 line 122
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1810Check line 124
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1811 line 126
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1811 line 128
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1811Check line 130
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1812 line 132
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1812 line 134
  63. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1812Check line 136
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1813 line 138
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1813 line 140
  66. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1813Check line 142
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1814 line 144
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1814 line 146
  69. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1814Check line 148
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1815 line 150
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1815 line 152
  72. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1815Check line 154
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1816 line 156
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1816 line 158
  75. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1816Check line 160
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1817 line 162
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1817 line 164
  78. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1817Check line 166
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1818 line 168
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1818 line 170
  81. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1818Check line 172
  82. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1819 line 174
  83. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1819 line 176
  84. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1819Check line 178
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1820 line 180
  86. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1820 line 182
  87. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1820Check line 184
  88. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1821 line 186
  89. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1821 line 188
  90. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1821Check line 190
  91. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1822 line 192
  92. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1822 line 194
  93. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1822Check line 196
  94. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1823 line 198
  95. def OAI.MUB6.Certificate.MixedTargetSemantics.originalMerge1823 line 200
  96. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMerge1823Check line 202