OAI/Analysis/MutuallyUnbiased/MixedSources/Rows23.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero368 line 40
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound368 line 109
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero369 line 114
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound369 line 183
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero370 line 188
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound370 line 257
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero371 line 262
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound371 line 331
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero372 line 336
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound372 line 405
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero373 line 410
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound373 line 434
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero374 line 439
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound374 line 463
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero375 line 468
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound375 line 495
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero376 line 500
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound376 line 527
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero377 line 532
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound377 line 556
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero378 line 561
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound378 line 585
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero379 line 590
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound379 line 614
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero380 line 619
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound380 line 688
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero381 line 693
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound381 line 714
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero382 line 719
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound382 line 743
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero383 line 748
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound383 line 775
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt368 line 780
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt369 line 783
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt370 line 786
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt371 line 789
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt372 line 792
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt373 line 795
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt374 line 798
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt375 line 801
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt376 line 804
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt377 line 807
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt378 line 810
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt379 line 813
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt380 line 816
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt381 line 819
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt382 line 822
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt383 line 825
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound23 line 828