OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionMergeSound29.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval928 line 16
  2. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval929 line 24
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval930 line 32
  4. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval931 line 40
  5. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval932 line 48
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval933 line 56
  7. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval934 line 64
  8. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval935 line 72
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval936 line 80
  10. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval937 line 88
  11. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval938 line 96
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval939 line 104
  13. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval940 line 112
  14. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval941 line 120
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval942 line 128
  16. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval943 line 136
  17. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval944 line 144
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval945 line 152
  19. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval946 line 160
  20. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval947 line 168
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval948 line 176
  22. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval949 line 184
  23. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval950 line 192
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval951 line 200
  25. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval952 line 208
  26. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval953 line 216
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval954 line 224
  28. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval955 line 232
  29. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval956 line 240
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval957 line 248
  31. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval958 line 256
  32. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval959 line 264