OAI/Analysis/MutuallyUnbiased/MixedSources/Rows34.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero544 line 46
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound544 line 70
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero545 line 75
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound545 line 123
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero546 line 128
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound546 line 197
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero547 line 202
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound547 line 271
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero548 line 276
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound548 line 345
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero549 line 350
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound549 line 374
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero550 line 379
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound550 line 403
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero551 line 408
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound551 line 477
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero552 line 482
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound552 line 551
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero553 line 556
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound553 line 625
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero554 line 630
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound554 line 699
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero555 line 704
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound555 line 773
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero556 line 778
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound556 line 802
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero557 line 807
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound557 line 876
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero558 line 881
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound558 line 950
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero559 line 955
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound559 line 979
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt544 line 984
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt545 line 987
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt546 line 990
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt547 line 993
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt548 line 996
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt549 line 999
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt550 line 1002
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt551 line 1005
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt552 line 1008
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt553 line 1011
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt554 line 1014
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt555 line 1017
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt556 line 1020
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt557 line 1023
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt558 line 1026
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt559 line 1029
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound34 line 1032