OAI/Analysis/MutuallyUnbiased/MixedSources/Rows30.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero480 line 51
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound480 line 78
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero481 line 83
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound481 line 152
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero482 line 157
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound482 line 226
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero483 line 231
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound483 line 300
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero484 line 305
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound484 line 374
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero485 line 379
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound485 line 448
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero486 line 453
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound486 line 477
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero487 line 482
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound487 line 575
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero488 line 580
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound488 line 673
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero489 line 678
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound489 line 771
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero490 line 776
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound490 line 803
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero491 line 808
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound491 line 835
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero492 line 840
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound492 line 864
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero493 line 869
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound493 line 896
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero494 line 901
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound494 line 928
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero495 line 933
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound495 line 960
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt480 line 965
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt481 line 968
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt482 line 971
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt483 line 974
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt484 line 977
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt485 line 980
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt486 line 983
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt487 line 986
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt488 line 989
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt489 line 992
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt490 line 995
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt491 line 998
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt492 line 1001
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt493 line 1004
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt494 line 1007
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt495 line 1010
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound30 line 1013