OAI/Analysis/MutuallyUnbiased/MixedSources/Rows42.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero672 line 43
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound672 line 70
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero673 line 75
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound673 line 102
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero674 line 107
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound674 line 134
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero675 line 139
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound675 line 232
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero676 line 237
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound676 line 264
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero677 line 269
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound677 line 296
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero678 line 301
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound678 line 328
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero679 line 333
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound679 line 360
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero680 line 365
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound680 line 389
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero681 line 394
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound681 line 418
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero682 line 423
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound682 line 468
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero683 line 473
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound683 line 518
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero684 line 523
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound684 line 544
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero685 line 549
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound685 line 570
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero686 line 575
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound686 line 620
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero687 line 625
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound687 line 670
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt672 line 675
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt673 line 678
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt674 line 681
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt675 line 684
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt676 line 687
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt677 line 690
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt678 line 693
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt679 line 696
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt680 line 699
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt681 line 702
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt682 line 705
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt683 line 708
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt684 line 711
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt685 line 714
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt686 line 717
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt687 line 720
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound42 line 723