OAI/Analysis/MutuallyUnbiased/MixedSources/Rows36.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero576 line 51
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound576 line 78
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero577 line 83
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound577 line 104
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero578 line 109
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound578 line 172
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero579 line 177
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound579 line 246
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero580 line 251
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound580 line 320
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero581 line 325
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound581 line 394
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero582 line 399
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound582 line 468
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero583 line 473
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound583 line 497
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero584 line 502
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound584 line 568
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero585 line 573
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound585 line 639
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero586 line 644
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound586 line 668
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero587 line 673
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound587 line 739
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero588 line 744
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound588 line 813
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero589 line 818
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound589 line 863
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero590 line 868
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound590 line 910
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero591 line 915
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound591 line 984
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt576 line 989
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt577 line 992
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt578 line 995
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt579 line 998
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt580 line 1001
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt581 line 1004
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt582 line 1007
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt583 line 1010
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt584 line 1013
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt585 line 1016
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt586 line 1019
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt587 line 1022
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt588 line 1025
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt589 line 1028
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt590 line 1031
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt591 line 1034
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound36 line 1037