OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionData37.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1184 line 11
  2. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1184 line 13
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1184 line 15
  4. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1185 line 19
  5. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1185 line 21
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1185 line 23
  7. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1186 line 27
  8. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1186 line 29
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1186 line 31
  10. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1187 line 35
  11. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1187 line 37
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1187 line 39
  13. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1188 line 44
  14. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1188 line 46
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1188 line 48
  16. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1189 line 53
  17. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1189 line 55
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1189 line 57
  19. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1190 line 62
  20. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1190 line 64
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1190 line 66
  22. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1191 line 70
  23. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1191 line 72
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1191 line 74
  25. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1192 line 78
  26. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1192 line 80
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1192 line 82
  28. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1193 line 86
  29. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1193 line 88
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1193 line 90
  31. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1194 line 94
  32. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1194 line 96
  33. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1194 line 98
  34. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1195 line 103
  35. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1195 line 105
  36. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1195 line 107
  37. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1196 line 112
  38. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1196 line 114
  39. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1196 line 116
  40. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1197 line 120
  41. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1197 line 122
  42. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1197 line 124
  43. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1198 line 129
  44. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1198 line 131
  45. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1198 line 133
  46. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1199 line 138
  47. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1199 line 140
  48. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1199 line 142
  49. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1200 line 146
  50. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1200 line 148
  51. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1200 line 150
  52. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1201 line 154
  53. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1201 line 156
  54. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1201 line 158
  55. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1202 line 163
  56. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1202 line 165
  57. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1202 line 167
  58. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1203 line 171
  59. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1203 line 173
  60. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1203 line 175
  61. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1204 line 179
  62. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1204 line 181
  63. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1204 line 183
  64. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1205 line 188
  65. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1205 line 190
  66. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1205 line 192
  67. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1206 line 197
  68. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1206 line 199
  69. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1206 line 201
  70. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1207 line 205
  71. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1207 line 207
  72. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1207 line 209
  73. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1208 line 213
  74. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1208 line 215
  75. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1208 line 217
  76. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1209 line 221
  77. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1209 line 223
  78. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1209 line 225
  79. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1210 line 229
  80. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1210 line 231
  81. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1210 line 233
  82. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1211 line 237
  83. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1211 line 239
  84. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1211 line 241
  85. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1212 line 245
  86. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1212 line 247
  87. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1212 line 249
  88. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1213 line 253
  89. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1213 line 255
  90. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1213 line 257
  91. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1214 line 261
  92. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1214 line 263
  93. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1214 line 265
  94. def OAI.MUB6.Certificate.MixedTargetSemantics.reducedTerm1215 line 269
  95. def OAI.MUB6.Certificate.MixedTargetSemantics.originalTerm1215 line 271
  96. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermArithmetic1215 line 273