OAI/Analysis/MutuallyUnbiased/MixedSources/Rows27.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero432 line 48
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound432 line 72
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero433 line 77
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound433 line 104
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero434 line 109
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound434 line 136
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero435 line 141
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound435 line 165
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero436 line 170
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound436 line 194
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero437 line 199
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound437 line 223
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero438 line 228
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound438 line 297
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero439 line 302
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound439 line 326
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero440 line 331
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound440 line 355
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero441 line 360
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound441 line 381
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero442 line 386
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound442 line 410
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero443 line 415
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound443 line 439
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero444 line 444
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound444 line 510
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero445 line 515
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound445 line 581
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero446 line 586
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound446 line 655
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero447 line 660
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound447 line 729
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt432 line 734
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt433 line 737
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt434 line 740
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt435 line 743
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt436 line 746
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt437 line 749
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt438 line 752
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt439 line 755
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt440 line 758
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt441 line 761
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt442 line 764
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt443 line 767
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt444 line 770
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt445 line 773
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt446 line 776
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt447 line 779
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound27 line 782