OAI/Analysis/MutuallyUnbiased/MixedSources/Rows41.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero656 line 55
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound656 line 121
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero657 line 126
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound657 line 192
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero658 line 197
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound658 line 266
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero659 line 271
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound659 line 340
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero660 line 345
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound660 line 405
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero661 line 410
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound661 line 434
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero662 line 439
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound662 line 460
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero663 line 465
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound663 line 561
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero664 line 566
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound664 line 662
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero665 line 667
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound665 line 694
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero666 line 699
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound666 line 795
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero667 line 800
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound667 line 896
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero668 line 901
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound668 line 997
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero669 line 1002
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound669 line 1029
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero670 line 1034
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound670 line 1061
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero671 line 1066
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound671 line 1090
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt656 line 1095
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt657 line 1098
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt658 line 1101
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt659 line 1104
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt660 line 1107
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt661 line 1110
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt662 line 1113
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt663 line 1116
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt664 line 1119
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt665 line 1122
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt666 line 1125
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt667 line 1128
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt668 line 1131
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt669 line 1134
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt670 line 1137
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt671 line 1140
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound41 line 1143