OAI/Analysis/MutuallyUnbiased/MixedSources/Rows44.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero704 line 46
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound704 line 67
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero705 line 72
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound705 line 93
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero706 line 98
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound706 line 128
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero707 line 133
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound707 line 163
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero708 line 168
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound708 line 198
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero709 line 203
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound709 line 233
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero710 line 238
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound710 line 307
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero711 line 312
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound711 line 381
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero712 line 386
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound712 line 455
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero713 line 460
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound713 line 484
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero714 line 489
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound714 line 513
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero715 line 518
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound715 line 539
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero716 line 544
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound716 line 568
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero717 line 573
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound717 line 642
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero718 line 647
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound718 line 716
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero719 line 721
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound719 line 790
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt704 line 795
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt705 line 798
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt706 line 801
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt707 line 804
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt708 line 807
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt709 line 810
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt710 line 813
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt711 line 816
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt712 line 819
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt713 line 822
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt714 line 825
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt715 line 828
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt716 line 831
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt717 line 834
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt718 line 837
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt719 line 840
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound44 line 843