OAI/Analysis/MutuallyUnbiased/MixedSources/Rows53.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero848 line 45
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound848 line 72
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero849 line 77
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound849 line 104
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero850 line 109
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound850 line 136
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero851 line 141
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound851 line 234
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero852 line 239
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound852 line 332
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero853 line 337
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound853 line 430
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero854 line 435
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound854 line 462
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero855 line 467
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound855 line 491
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero856 line 496
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound856 line 520
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero857 line 525
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound857 line 618
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero858 line 623
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound858 line 719
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero859 line 724
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound859 line 820
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero860 line 825
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound860 line 852
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero861 line 857
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound861 line 884
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero862 line 889
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound862 line 916
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero863 line 921
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound863 line 990
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt848 line 995
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt849 line 998
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt850 line 1001
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt851 line 1004
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt852 line 1007
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt853 line 1010
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt854 line 1013
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt855 line 1016
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt856 line 1019
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt857 line 1022
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt858 line 1025
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt859 line 1028
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt860 line 1031
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt861 line 1034
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt862 line 1037
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt863 line 1040
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound53 line 1043