OAI/Analysis/MutuallyUnbiased/MixedSources/Rows48.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero768 line 34
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound768 line 61
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero769 line 66
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound769 line 159
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero770 line 164
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound770 line 191
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero771 line 196
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound771 line 223
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero772 line 228
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound772 line 252
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero773 line 257
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound773 line 284
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero774 line 289
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound774 line 316
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero775 line 321
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound775 line 348
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero776 line 353
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound776 line 377
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero777 line 382
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound777 line 406
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero778 line 411
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound778 line 438
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero779 line 443
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound779 line 539
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero780 line 544
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound780 line 640
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero781 line 645
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound781 line 672
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero782 line 677
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound782 line 698
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero783 line 703
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound783 line 730
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt768 line 735
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt769 line 738
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt770 line 741
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt771 line 744
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt772 line 747
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt773 line 750
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt774 line 753
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt775 line 756
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt776 line 759
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt777 line 762
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt778 line 765
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt779 line 768
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt780 line 771
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt781 line 774
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt782 line 777
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt783 line 780
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound48 line 783