OAI/Analysis/MutuallyUnbiased/MixedSources/Rows26.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero416 line 48
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound416 line 75
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero417 line 80
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound417 line 149
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero418 line 154
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound418 line 223
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero419 line 228
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound419 line 297
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero420 line 302
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound420 line 326
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero421 line 331
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound421 line 355
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero422 line 360
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound422 line 384
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero423 line 389
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound423 line 416
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero424 line 421
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound424 line 448
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero425 line 453
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound425 line 477
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero426 line 482
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound426 line 551
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero427 line 556
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound427 line 625
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero428 line 630
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound428 line 699
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero429 line 704
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound429 line 728
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero430 line 733
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound430 line 757
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero431 line 762
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound431 line 786
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt416 line 791
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt417 line 794
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt418 line 797
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt419 line 800
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt420 line 803
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt421 line 806
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt422 line 809
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt423 line 812
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt424 line 815
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt425 line 818
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt426 line 821
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt427 line 824
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt428 line 827
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt429 line 830
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt430 line 833
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt431 line 836
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound26 line 839