OAI/Analysis/MutuallyUnbiased/MixedTargets/ReductionMergeSound44.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1408 line 15
  2. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1409 line 23
  3. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1410 line 31
  4. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1411 line 39
  5. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1412 line 47
  6. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1413 line 55
  7. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1414 line 63
  8. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1415 line 71
  9. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1416 line 79
  10. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1417 line 87
  11. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1418 line 95
  12. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1419 line 103
  13. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1420 line 111
  14. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1421 line 119
  15. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1422 line 127
  16. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1423 line 135
  17. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1424 line 143
  18. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1425 line 151
  19. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1426 line 159
  20. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1427 line 167
  21. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1428 line 175
  22. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1429 line 183
  23. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1430 line 191
  24. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1431 line 199
  25. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1432 line 207
  26. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1433 line 215
  27. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1434 line 223
  28. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1435 line 231
  29. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1436 line 239
  30. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1437 line 247
  31. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1438 line 255
  32. theorem OAI.MUB6.Certificate.MixedTargetSemantics.reducedMergeEval1439 line 263