OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionMergeSound59.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1888 line 16
  2. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1889 line 24
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1890 line 32
  4. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1891 line 40
  5. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1892 line 48
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1893 line 56
  7. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1894 line 64
  8. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1895 line 72
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1896 line 80
  10. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1897 line 88
  11. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1898 line 96
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1899 line 104
  13. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1900 line 112
  14. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1901 line 120
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1902 line 128
  16. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1903 line 136
  17. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1904 line 144
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1905 line 152
  19. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1906 line 160
  20. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1907 line 168
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1908 line 176
  22. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1909 line 184
  23. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1910 line 192
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1911 line 200
  25. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1912 line 208
  26. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1913 line 216
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1914 line 224
  28. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1915 line 232
  29. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1916 line 240
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1917 line 248