OAI/Analysis/MutuallyUnbiased/MixedSources/Rows117.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1872 line 51
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1872 line 120
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1873 line 125
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1873 line 194
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1874 line 199
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1874 line 268
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1875 line 273
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1875 line 342
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1876 line 347
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1876 line 371
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1877 line 376
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1877 line 445
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1878 line 450
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1878 line 519
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1879 line 524
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1879 line 548
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1880 line 553
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1880 line 649
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1881 line 654
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1881 line 747
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1882 line 752
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1882 line 800
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1883 line 805
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1883 line 832
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1884 line 837
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1884 line 861
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1885 line 866
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1885 line 890
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1886 line 895
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1886 line 919
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1887 line 924
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1887 line 951
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1872 line 956
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1873 line 959
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1874 line 962
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1875 line 965
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1876 line 968
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1877 line 971
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1878 line 974
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1879 line 977
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1880 line 980
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1881 line 983
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1882 line 986
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1883 line 989
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1884 line 992
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1885 line 995
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1886 line 998
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1887 line 1001
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound117 line 1004