OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionSound55.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1760 line 13
  2. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1761 line 22
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1762 line 31
  4. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1763 line 40
  5. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1764 line 49
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1765 line 58
  7. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1766 line 67
  8. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1767 line 76
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1768 line 85
  10. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1769 line 94
  11. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1770 line 103
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1771 line 112
  13. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1772 line 121
  14. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1773 line 130
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1774 line 139
  16. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1775 line 148
  17. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1776 line 157
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1777 line 166
  19. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1778 line 175
  20. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1779 line 184
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1780 line 193
  22. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1781 line 202
  23. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1782 line 211
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1783 line 220
  25. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1784 line 229
  26. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1785 line 238
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1786 line 247
  28. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1787 line 256
  29. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1788 line 265
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1789 line 274
  31. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1790 line 283
  32. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1791 line 292