OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionData59.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1888 line 11
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1888 line 13
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1888 line 15
  4. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1889 line 19
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1889 line 21
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1889 line 23
  7. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1890 line 27
  8. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1890 line 29
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1890 line 31
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1891 line 36
  11. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1891 line 38
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1891 line 40
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1892 line 45
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1892 line 47
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1892 line 49
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1893 line 53
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1893 line 55
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1893 line 57
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1894 line 61
  20. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1894 line 63
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1894 line 65
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1895 line 69
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1895 line 71
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1895 line 73
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1896 line 78
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1896 line 80
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1896 line 82
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1897 line 86
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1897 line 88
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1897 line 90
  31. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1898 line 94
  32. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1898 line 96
  33. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1898 line 98
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1899 line 103
  35. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1899 line 105
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1899 line 107
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1900 line 112
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1900 line 114
  39. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1900 line 116
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1901 line 120
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1901 line 122
  42. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1901 line 124
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1902 line 129
  44. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1902 line 131
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1902 line 133
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1903 line 138
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1903 line 140
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1903 line 142
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1904 line 146
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1904 line 148
  51. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1904 line 150
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1905 line 154
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1905 line 156
  54. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1905 line 158
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1906 line 163
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1906 line 165
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1906 line 167
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1907 line 172
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1907 line 174
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1907 line 176
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1908 line 181
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1908 line 183
  63. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1908 line 185
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1909 line 189
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1909 line 191
  66. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1909 line 193
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1910 line 197
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1910 line 199
  69. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1910 line 201
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1911 line 205
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1911 line 207
  72. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1911 line 209
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1912 line 213
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1912 line 215
  75. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1912 line 217
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1913 line 222
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1913 line 224
  78. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1913 line 226
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1914 line 231
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1914 line 233
  81. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1914 line 235
  82. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1915 line 239
  83. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1915 line 241
  84. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1915 line 243
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1916 line 248
  86. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1916 line 250
  87. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1916 line 252
  88. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1917 line 257
  89. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1917 line 259
  90. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1917 line 261
  91. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1918 line 265
  92. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1918 line 267
  93. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1918 line 269