OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionData58.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1856 line 12
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1856 line 14
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1856 line 16
  4. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1857 line 21
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1857 line 23
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1857 line 25
  7. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1858 line 30
  8. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1858 line 32
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1858 line 34
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1859 line 38
  11. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1859 line 40
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1859 line 42
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1860 line 47
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1860 line 49
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1860 line 51
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1861 line 56
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1861 line 58
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1861 line 60
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1862 line 64
  20. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1862 line 66
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1862 line 68
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1863 line 72
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1863 line 74
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1863 line 76
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1864 line 80
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1864 line 82
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1864 line 84
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1865 line 88
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1865 line 90
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1865 line 92
  31. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1866 line 96
  32. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1866 line 98
  33. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1866 line 100
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1867 line 104
  35. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1867 line 106
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1867 line 108
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1868 line 112
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1868 line 114
  39. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1868 line 116
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1869 line 120
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1869 line 122
  42. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1869 line 124
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1870 line 128
  44. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1870 line 130
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1870 line 132
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1871 line 136
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1871 line 138
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1871 line 140
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1872 line 144
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1872 line 146
  51. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1872 line 148
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1873 line 152
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1873 line 154
  54. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1873 line 156
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1874 line 160
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1874 line 162
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1874 line 164
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1875 line 168
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1875 line 170
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1875 line 172
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1876 line 176
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1876 line 178
  63. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1876 line 180
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1877 line 184
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1877 line 186
  66. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1877 line 188
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1878 line 193
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1878 line 195
  69. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1878 line 197
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1879 line 202
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1879 line 204
  72. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1879 line 206
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1880 line 210
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1880 line 212
  75. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1880 line 214
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1881 line 218
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1881 line 220
  78. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1881 line 222
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1882 line 226
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1882 line 228
  81. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1882 line 230
  82. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1883 line 234
  83. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1883 line 236
  84. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1883 line 238
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1884 line 243
  86. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1884 line 245
  87. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1884 line 247
  88. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1885 line 252
  89. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1885 line 254
  90. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1885 line 256
  91. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1886 line 260
  92. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1886 line 262
  93. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1886 line 264
  94. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1887 line 268
  95. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1887 line 270
  96. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1887 line 272