OAI/Analysis/MutuallyUnbiased/MixedSources/Rows126.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2016 line 50
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2016 line 95
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2017 line 100
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2017 line 145
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2018 line 150
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2018 line 195
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2019 line 200
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2019 line 248
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2020 line 253
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2020 line 301
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2021 line 306
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2021 line 354
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2022 line 359
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2022 line 407
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2023 line 412
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2023 line 481
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2024 line 486
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2024 line 555
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2025 line 560
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2025 line 587
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2026 line 592
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2026 line 619
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2027 line 624
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2027 line 651
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2028 line 656
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2028 line 683
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2029 line 688
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2029 line 715
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2030 line 720
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2030 line 747
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2031 line 752
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2031 line 776
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2016 line 781
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2017 line 784
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2018 line 787
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2019 line 790
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2020 line 793
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2021 line 796
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2022 line 799
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2023 line 802
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2024 line 805
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2025 line 808
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2026 line 811
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2027 line 814
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2028 line 817
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2029 line 820
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2030 line 823
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2031 line 826
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound126 line 829