OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionMergeSound52.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1664 line 14
  2. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1665 line 22
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1666 line 30
  4. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1667 line 38
  5. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1668 line 46
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1669 line 54
  7. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1670 line 62
  8. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1671 line 70
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1672 line 78
  10. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1673 line 86
  11. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1674 line 94
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1675 line 102
  13. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1676 line 110
  14. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1677 line 118
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1678 line 126
  16. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1679 line 134
  17. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1680 line 142
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1681 line 150
  19. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1682 line 158
  20. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1683 line 166
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1684 line 174
  22. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1685 line 182
  23. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1686 line 190
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1687 line 198
  25. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1688 line 206
  26. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1689 line 214
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1690 line 222
  28. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1691 line 230
  29. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1692 line 238
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1693 line 246
  31. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1694 line 254
  32. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1695 line 262