OAI/Analysis/MutuallyUnbiased/MixedSources/Rows38.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero608 line 58
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound608 line 127
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero609 line 132
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound609 line 150
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero610 line 155
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound610 line 179
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero611 line 184
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound611 line 208
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero612 line 213
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound612 line 282
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero613 line 287
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound613 line 356
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero614 line 361
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound614 line 430
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero615 line 435
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound615 line 459
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero616 line 464
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound616 line 488
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero617 line 493
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound617 line 514
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero618 line 519
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound618 line 543
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero619 line 548
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound619 line 572
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero620 line 577
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound620 line 640
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero621 line 645
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound621 line 714
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero622 line 719
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound622 line 788
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero623 line 793
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound623 line 817
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt608 line 822
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt609 line 825
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt610 line 828
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt611 line 831
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt612 line 834
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt613 line 837
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt614 line 840
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt615 line 843
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt616 line 846
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt617 line 849
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt618 line 852
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt619 line 855
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt620 line 858
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt621 line 861
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt622 line 864
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt623 line 867
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound38 line 870