OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionSound39.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1248 line 13
  2. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1249 line 22
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1250 line 31
  4. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1251 line 40
  5. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1252 line 49
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1253 line 58
  7. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1254 line 67
  8. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1255 line 76
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1256 line 85
  10. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1257 line 94
  11. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1258 line 103
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1259 line 112
  13. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1260 line 121
  14. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1261 line 130
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1262 line 139
  16. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1263 line 148
  17. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1264 line 157
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1265 line 166
  19. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1266 line 175
  20. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1267 line 184
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1268 line 193
  22. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1269 line 202
  23. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1270 line 211
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1271 line 220
  25. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1272 line 229
  26. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1273 line 238
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1274 line 247
  28. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1275 line 256
  29. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1276 line 265
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1277 line 274
  31. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1278 line 283
  32. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1279 line 292