OAI/Analysis/MutuallyUnbiased/MixedSources/Rows45.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero720 line 52
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound720 line 121
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero721 line 126
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound721 line 195
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero722 line 200
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound722 line 269
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero723 line 274
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound723 line 343
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero724 line 348
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound724 line 369
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero725 line 374
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound725 line 398
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero726 line 403
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound726 line 472
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero727 line 477
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound727 line 546
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero728 line 551
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound728 line 608
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero729 line 613
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound729 line 682
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero730 line 687
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound730 line 756
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero731 line 761
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound731 line 830
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero732 line 835
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound732 line 904
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero733 line 909
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound733 line 978
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero734 line 983
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound734 line 1052
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero735 line 1057
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound735 line 1114
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt720 line 1119
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt721 line 1122
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt722 line 1125
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt723 line 1128
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt724 line 1131
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt725 line 1134
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt726 line 1137
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt727 line 1140
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt728 line 1143
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt729 line 1146
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt730 line 1149
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt731 line 1152
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt732 line 1155
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt733 line 1158
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt734 line 1161
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt735 line 1164
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound45 line 1167