OAI/Analysis/MutuallyUnbiased/MixedSources/Rows1.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero16 line 27
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound16 line 96
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero17 line 101
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound17 line 146
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero18 line 151
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound18 line 232
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero19 line 237
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound19 line 330
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero20 line 335
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound20 line 389
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero21 line 394
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound21 line 424
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero22 line 429
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound22 line 477
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero23 line 482
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound23 line 530
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero24 line 535
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound24 line 601
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero25 line 606
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound25 line 636
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero26 line 641
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound26 line 662
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero27 line 667
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound27 line 706
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero28 line 711
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound28 line 768
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero29 line 773
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound29 line 797
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero30 line 802
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound30 line 823
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero31 line 828
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound31 line 849
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt16 line 854
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt17 line 857
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt18 line 860
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt19 line 863
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt20 line 866
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt21 line 869
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt22 line 872
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt23 line 875
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt24 line 878
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt25 line 881
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt26 line 884
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt27 line 887
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt28 line 890
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt29 line 893
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt30 line 896
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt31 line 899
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound1 line 902