OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionMergeSound14.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval448 line 15
  2. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval449 line 23
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval450 line 31
  4. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval451 line 39
  5. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval452 line 47
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval453 line 55
  7. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval454 line 63
  8. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval455 line 71
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval456 line 79
  10. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval457 line 87
  11. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval458 line 95
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval459 line 103
  13. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval460 line 111
  14. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval461 line 119
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval462 line 127
  16. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval463 line 135
  17. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval464 line 143
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval465 line 151
  19. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval466 line 159
  20. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval467 line 167
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval468 line 175
  22. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval469 line 183
  23. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval470 line 191
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval471 line 199
  25. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval472 line 207
  26. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval473 line 215
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval474 line 223
  28. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval475 line 231
  29. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval476 line 239
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval477 line 247
  31. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval478 line 255
  32. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval479 line 263