OAI/Analysis/MutuallyUnbiased/MixedSources/Rows106.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1696 line 67
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1696 line 91
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1697 line 96
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1697 line 123
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1698 line 128
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1698 line 155
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1699 line 160
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1699 line 187
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1700 line 192
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1700 line 219
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1701 line 224
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1701 line 251
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1702 line 256
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1702 line 325
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1703 line 330
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1703 line 399
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1704 line 404
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1704 line 473
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1705 line 478
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1705 line 502
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1706 line 507
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1706 line 534
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1707 line 539
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1707 line 563
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1708 line 568
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1708 line 637
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1709 line 642
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1709 line 711
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1710 line 716
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1710 line 812
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1711 line 817
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1711 line 913
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1696 line 918
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1697 line 921
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1698 line 924
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1699 line 927
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1700 line 930
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1701 line 933
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1702 line 936
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1703 line 939
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1704 line 942
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1705 line 945
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1706 line 948
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1707 line 951
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1708 line 954
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1709 line 957
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1710 line 960
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1711 line 963
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound106 line 966