OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionSound50.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1600 line 13
  2. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1601 line 22
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1602 line 31
  4. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1603 line 40
  5. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1604 line 49
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1605 line 58
  7. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1606 line 67
  8. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1607 line 76
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1608 line 85
  10. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1609 line 94
  11. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1610 line 103
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1611 line 112
  13. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1612 line 121
  14. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1613 line 130
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1614 line 139
  16. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1615 line 148
  17. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1616 line 157
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1617 line 166
  19. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1618 line 175
  20. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1619 line 184
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1620 line 193
  22. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1621 line 202
  23. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1622 line 211
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1623 line 220
  25. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1624 line 229
  26. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1625 line 238
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1626 line 247
  28. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1627 line 256
  29. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1628 line 265
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1629 line 274
  31. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1630 line 283
  32. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1631 line 292