OAI/Analysis/MutuallyUnbiased/MixedSources/Rows103.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1648 line 62
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1648 line 107
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1649 line 112
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1649 line 157
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1650 line 162
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1650 line 207
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1651 line 212
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1651 line 257
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1652 line 262
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1652 line 331
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1653 line 336
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1653 line 405
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1654 line 410
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1654 line 449
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1655 line 454
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1655 line 523
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1656 line 528
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1656 line 597
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1657 line 602
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1657 line 671
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1658 line 676
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1658 line 745
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1659 line 750
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1659 line 774
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1660 line 779
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1660 line 806
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1661 line 811
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1661 line 877
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1662 line 882
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1662 line 951
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1663 line 956
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1663 line 983
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1648 line 988
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1649 line 991
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1650 line 994
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1651 line 997
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1652 line 1000
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1653 line 1003
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1654 line 1006
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1655 line 1009
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1656 line 1012
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1657 line 1015
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1658 line 1018
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1659 line 1021
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1660 line 1024
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1661 line 1027
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1662 line 1030
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1663 line 1033
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound103 line 1036