OAI/Analysis/MutuallyUnbiased/MixedSources/Rows111.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1776 line 59
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1776 line 83
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1777 line 88
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1777 line 112
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1778 line 117
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1778 line 141
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1779 line 146
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1779 line 173
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1780 line 178
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1780 line 247
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1781 line 252
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1781 line 321
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1782 line 326
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1782 line 395
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1783 line 400
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1783 line 469
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1784 line 474
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1784 line 534
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1785 line 539
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1785 line 608
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1786 line 613
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1786 line 661
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1787 line 666
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1787 line 714
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1788 line 719
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1788 line 767
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1789 line 772
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1789 line 820
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1790 line 825
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1790 line 867
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1791 line 872
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1791 line 890
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1776 line 895
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1777 line 898
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1778 line 901
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1779 line 904
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1780 line 907
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1781 line 910
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1782 line 913
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1783 line 916
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1784 line 919
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1785 line 922
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1786 line 925
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1787 line 928
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1788 line 931
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1789 line 934
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1790 line 937
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1791 line 940
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound111 line 943