OAI/Analysis/MutuallyUnbiased/MixedSources/Rows51.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero816 line 41
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound816 line 110
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero817 line 115
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound817 line 184
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero818 line 189
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound818 line 258
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero819 line 263
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound819 line 287
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero820 line 292
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound820 line 319
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero821 line 324
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound821 line 393
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero822 line 398
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound822 line 467
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero823 line 472
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound823 line 541
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero824 line 546
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound824 line 570
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero825 line 575
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound825 line 599
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero826 line 604
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound826 line 625
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero827 line 630
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound827 line 654
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero828 line 659
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound828 line 686
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero829 line 691
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound829 line 715
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero830 line 720
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound830 line 744
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero831 line 749
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound831 line 773
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt816 line 778
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt817 line 781
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt818 line 784
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt819 line 787
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt820 line 790
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt821 line 793
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt822 line 796
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt823 line 799
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt824 line 802
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt825 line 805
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt826 line 808
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt827 line 811
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt828 line 814
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt829 line 817
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt830 line 820
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt831 line 823
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound51 line 826