OAI/Analysis/MutuallyUnbiased/MixedSources/Rows128.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2048 line 39
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2048 line 63
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2049 line 68
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2049 line 92
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2050 line 97
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2050 line 115
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2051 line 120
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2051 line 189
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2052 line 194
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2052 line 263
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2053 line 268
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2053 line 292
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2054 line 297
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2054 line 321
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2055 line 326
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2055 line 350
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2056 line 355
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2056 line 400
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2057 line 405
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2057 line 450
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2058 line 455
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2058 line 479
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2059 line 484
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2059 line 553
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2060 line 558
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2060 line 627
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2061 line 632
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2061 line 701
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2062 line 706
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2062 line 799
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2063 line 804
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2063 line 861
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2048 line 866
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2049 line 869
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2050 line 872
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2051 line 875
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2052 line 878
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2053 line 881
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2054 line 884
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2055 line 887
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2056 line 890
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2057 line 893
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2058 line 896
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2059 line 899
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2060 line 902
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2061 line 905
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2062 line 908
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2063 line 911
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound128 line 914