OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionSound58.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1856 line 12
  2. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1857 line 21
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1858 line 30
  4. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1859 line 39
  5. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1860 line 48
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1861 line 57
  7. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1862 line 66
  8. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1863 line 75
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1864 line 84
  10. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1865 line 93
  11. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1866 line 102
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1867 line 111
  13. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1868 line 120
  14. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1869 line 129
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1870 line 138
  16. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1871 line 147
  17. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1872 line 156
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1873 line 165
  19. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1874 line 174
  20. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1875 line 183
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1876 line 192
  22. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1877 line 201
  23. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1878 line 210
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1879 line 219
  25. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1880 line 228
  26. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1881 line 237
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1882 line 246
  28. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1883 line 255
  29. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1884 line 264
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1885 line 273
  31. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1886 line 282
  32. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedTermEval1887 line 291