OAI/Analysis/MutuallyUnbiased/MixedSources/Rows115.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1840 line 57
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1840 line 126
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1841 line 131
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1841 line 200
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1842 line 205
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1842 line 229
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1843 line 234
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1843 line 261
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1844 line 266
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1844 line 335
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1845 line 340
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1845 line 409
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1846 line 414
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1846 line 483
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1847 line 488
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1847 line 557
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1848 line 562
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1848 line 610
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1849 line 615
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1849 line 663
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1850 line 668
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1850 line 716
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1851 line 721
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1851 line 742
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1852 line 747
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1852 line 771
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1853 line 776
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1853 line 824
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1854 line 829
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1854 line 877
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1855 line 882
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1855 line 930
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1840 line 935
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1841 line 938
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1842 line 941
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1843 line 944
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1844 line 947
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1845 line 950
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1846 line 953
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1847 line 956
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1848 line 959
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1849 line 962
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1850 line 965
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1851 line 968
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1852 line 971
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1853 line 974
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1854 line 977
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1855 line 980
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound115 line 983