OAI/Analysis/MutuallyUnbiased/MixedSources/Rows120.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1920 line 50
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1920 line 74
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1921 line 79
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1921 line 103
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1922 line 108
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1922 line 132
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1923 line 137
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1923 line 164
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1924 line 169
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1924 line 265
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1925 line 270
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1925 line 366
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1926 line 371
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1926 line 467
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1927 line 472
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1927 line 499
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1928 line 504
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1928 line 525
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1929 line 530
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1929 line 551
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1930 line 556
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1930 line 580
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1931 line 585
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1931 line 612
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1932 line 617
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1932 line 641
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1933 line 646
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1933 line 670
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1934 line 675
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1934 line 702
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1935 line 707
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1935 line 776
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1920 line 781
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1921 line 784
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1922 line 787
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1923 line 790
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1924 line 793
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1925 line 796
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1926 line 799
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1927 line 802
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1928 line 805
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1929 line 808
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1930 line 811
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1931 line 814
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1932 line 817
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1933 line 820
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1934 line 823
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1935 line 826
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound120 line 829