OAI/Analysis/MutuallyUnbiased/MixedSources/Rows52.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero832 line 41
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound832 line 65
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero833 line 70
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound833 line 139
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero834 line 144
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound834 line 213
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero835 line 218
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound835 line 242
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero836 line 247
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound836 line 271
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero837 line 276
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound837 line 300
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero838 line 305
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound838 line 329
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero839 line 334
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound839 line 358
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero840 line 363
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound840 line 432
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero841 line 437
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound841 line 506
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero842 line 511
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound842 line 580
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero843 line 585
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound843 line 648
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero844 line 653
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound844 line 722
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero845 line 727
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound845 line 796
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero846 line 801
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound846 line 825
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero847 line 830
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound847 line 926
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt832 line 931
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt833 line 934
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt834 line 937
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt835 line 940
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt836 line 943
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt837 line 946
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt838 line 949
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt839 line 952
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt840 line 955
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt841 line 958
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt842 line 961
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt843 line 964
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt844 line 967
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt845 line 970
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt846 line 973
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt847 line 976
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound52 line 979