OAI/Analysis/MutuallyUnbiased/MixedSources/Rows94.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1504 line 40
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1504 line 64
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1505 line 69
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1505 line 138
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1506 line 143
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1506 line 212
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1507 line 217
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1507 line 286
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1508 line 291
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1508 line 360
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1509 line 365
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1509 line 434
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1510 line 439
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1510 line 508
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1511 line 513
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1511 line 582
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1512 line 587
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1512 line 611
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1513 line 616
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1513 line 664
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1514 line 669
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1514 line 738
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1515 line 743
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1515 line 767
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1516 line 772
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1516 line 820
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1517 line 825
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1517 line 873
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1518 line 878
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1518 line 926
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1519 line 931
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1519 line 952
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1504 line 957
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1505 line 960
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1506 line 963
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1507 line 966
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1508 line 969
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1509 line 972
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1510 line 975
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1511 line 978
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1512 line 981
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1513 line 984
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1514 line 987
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1515 line 990
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1516 line 993
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1517 line 996
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1518 line 999
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1519 line 1002
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound94 line 1005