OAI/Analysis/MutuallyUnbiased/MixedSources/Rows116.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1856 line 55
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1856 line 103
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1857 line 108
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1857 line 135
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1858 line 140
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1858 line 236
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1859 line 241
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1859 line 337
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1860 line 342
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1860 line 438
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1861 line 443
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1861 line 470
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1862 line 475
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1862 line 502
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1863 line 507
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1863 line 534
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1864 line 539
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1864 line 635
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1865 line 640
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1865 line 709
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1866 line 714
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1866 line 783
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1867 line 788
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1867 line 857
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1868 line 862
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1868 line 886
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1869 line 891
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1869 line 915
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1870 line 920
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1870 line 944
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1871 line 949
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1871 line 1018
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1856 line 1023
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1857 line 1026
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1858 line 1029
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1859 line 1032
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1860 line 1035
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1861 line 1038
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1862 line 1041
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1863 line 1044
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1864 line 1047
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1865 line 1050
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1866 line 1053
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1867 line 1056
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1868 line 1059
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1869 line 1062
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1870 line 1065
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1871 line 1068
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound116 line 1071