OAI/Analysis/MutuallyUnbiased/MixedSources/Rows127.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2032 line 52
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2032 line 76
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2033 line 81
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2033 line 126
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2034 line 131
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2034 line 176
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2035 line 181
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2035 line 211
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2036 line 216
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2036 line 264
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2037 line 269
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2037 line 317
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2038 line 322
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2038 line 355
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2039 line 360
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2039 line 456
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2040 line 461
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2040 line 557
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2041 line 562
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2041 line 658
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2042 line 663
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2042 line 690
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2043 line 695
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2043 line 722
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2044 line 727
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2044 line 754
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2045 line 759
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2045 line 828
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2046 line 833
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2046 line 902
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2047 line 907
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2047 line 976
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2032 line 981
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2033 line 984
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2034 line 987
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2035 line 990
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2036 line 993
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2037 line 996
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2038 line 999
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2039 line 1002
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2040 line 1005
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2041 line 1008
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2042 line 1011
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2043 line 1014
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2044 line 1017
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2045 line 1020
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2046 line 1023
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2047 line 1026
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound127 line 1029