OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionData6.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm192 line 10
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm192 line 12
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic192 line 14
  4. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm193 line 19
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm193 line 21
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic193 line 23
  7. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm194 line 27
  8. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm194 line 29
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic194 line 31
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm195 line 35
  11. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm195 line 37
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic195 line 39
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm196 line 43
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm196 line 45
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic196 line 47
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm197 line 52
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm197 line 54
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic197 line 56
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm198 line 61
  20. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm198 line 63
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic198 line 65
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm199 line 70
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm199 line 72
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic199 line 74
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm200 line 79
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm200 line 81
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic200 line 83
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm201 line 87
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm201 line 89
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic201 line 91
  31. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm202 line 96
  32. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm202 line 98
  33. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic202 line 100
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm203 line 105
  35. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm203 line 107
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic203 line 109
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm204 line 114
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm204 line 116
  39. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic204 line 118
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm205 line 123
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm205 line 125
  42. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic205 line 127
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm206 line 132
  44. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm206 line 134
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic206 line 136
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm207 line 141
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm207 line 143
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic207 line 145
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm208 line 150
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm208 line 152
  51. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic208 line 154
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm209 line 159
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm209 line 161
  54. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic209 line 163
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm210 line 168
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm210 line 170
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic210 line 172
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm211 line 177
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm211 line 179
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic211 line 181
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm212 line 186
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm212 line 188
  63. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic212 line 190
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm213 line 195
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm213 line 197
  66. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic213 line 199
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm214 line 204
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm214 line 206
  69. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic214 line 208
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm215 line 213
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm215 line 215
  72. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic215 line 217
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm216 line 222
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm216 line 224
  75. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic216 line 226
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm217 line 231
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm217 line 233
  78. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic217 line 235
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm218 line 240
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm218 line 242
  81. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic218 line 244
  82. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm219 line 249
  83. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm219 line 251
  84. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic219 line 253
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm220 line 258
  86. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm220 line 260
  87. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic220 line 262
  88. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm221 line 267
  89. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm221 line 269
  90. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic221 line 271
  91. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm222 line 276
  92. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm222 line 278
  93. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic222 line 280
  94. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm223 line 285
  95. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm223 line 287
  96. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic223 line 289