OAI/Analysis/MutuallyUnbiased/MixedSources/Rows33.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero528 line 50
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound528 line 77
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero529 line 82
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound529 line 106
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero530 line 111
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound530 line 135
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero531 line 140
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound531 line 209
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero532 line 214
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound532 line 283
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero533 line 288
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound533 line 357
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero534 line 362
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound534 line 431
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero535 line 436
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound535 line 460
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero536 line 465
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound536 line 534
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero537 line 539
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound537 line 608
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero538 line 613
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound538 line 682
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero539 line 687
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound539 line 756
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero540 line 761
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound540 line 830
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero541 line 835
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound541 line 880
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero542 line 885
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound542 line 951
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero543 line 956
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound543 line 1025
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt528 line 1030
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt529 line 1033
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt530 line 1036
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt531 line 1039
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt532 line 1042
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt533 line 1045
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt534 line 1048
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt535 line 1051
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt536 line 1054
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt537 line 1057
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt538 line 1060
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt539 line 1063
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt540 line 1066
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt541 line 1069
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt542 line 1072
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt543 line 1075
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound33 line 1078