OAI/Analysis/MutuallyUnbiased/MixedSources/Rows47.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero752 line 39
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound752 line 66
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero753 line 71
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound753 line 98
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero754 line 103
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound754 line 130
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero755 line 135
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound755 line 162
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero756 line 167
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound756 line 185
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero757 line 190
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound757 line 280
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero758 line 285
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound758 line 381
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero759 line 386
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound759 line 479
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero760 line 484
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound760 line 511
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero761 line 516
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound761 line 543
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero762 line 548
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound762 line 575
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero763 line 580
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound763 line 607
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero764 line 612
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound764 line 639
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero765 line 644
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound765 line 671
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero766 line 676
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound766 line 703
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero767 line 708
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound767 line 735
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt752 line 740
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt753 line 743
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt754 line 746
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt755 line 749
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt756 line 752
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt757 line 755
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt758 line 758
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt759 line 761
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt760 line 764
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt761 line 767
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt762 line 770
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt763 line 773
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt764 line 776
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt765 line 779
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt766 line 782
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt767 line 785
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound47 line 788