OAI/Analysis/MutuallyUnbiased/MixedSources/Rows50.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero800 line 46
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound800 line 139
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero801 line 144
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound801 line 198
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero802 line 203
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound802 line 299
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero803 line 304
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound803 line 331
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero804 line 336
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound804 line 429
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero805 line 434
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound805 line 530
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero806 line 535
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound806 line 562
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero807 line 567
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound807 line 594
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero808 line 599
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound808 line 626
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero809 line 631
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound809 line 658
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero810 line 663
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound810 line 690
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero811 line 695
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound811 line 722
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero812 line 727
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound812 line 754
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero813 line 759
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound813 line 822
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero814 line 827
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound814 line 911
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero815 line 916
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound815 line 1009
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt800 line 1014
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt801 line 1017
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt802 line 1020
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt803 line 1023
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt804 line 1026
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt805 line 1029
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt806 line 1032
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt807 line 1035
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt808 line 1038
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt809 line 1041
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt810 line 1044
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt811 line 1047
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt812 line 1050
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt813 line 1053
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt814 line 1056
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt815 line 1059
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound50 line 1062