OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionMergeSound0.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval0 line 11
  2. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1 line 19
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval2 line 27
  4. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval3 line 35
  5. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval4 line 43
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval5 line 51
  7. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval6 line 59
  8. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval7 line 67
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval8 line 75
  10. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval9 line 83
  11. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval10 line 91
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval11 line 99
  13. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval12 line 107
  14. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval13 line 115
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval14 line 123
  16. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval15 line 131
  17. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval16 line 139
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval17 line 147
  19. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval18 line 155
  20. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval19 line 163
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval20 line 171
  22. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval21 line 179
  23. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval22 line 187
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval23 line 195
  25. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval24 line 203
  26. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval25 line 211
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval26 line 219
  28. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval27 line 227
  29. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval28 line 235
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval29 line 243
  31. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval30 line 251
  32. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval31 line 259