OAI/Analysis/MutuallyUnbiased/MixedSources/Rows131.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2096 line 37
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2096 line 106
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2097 line 111
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2097 line 180
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2098 line 185
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2098 line 230
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2099 line 235
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2099 line 280
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2100 line 285
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2100 line 330
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2101 line 335
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2101 line 380
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2102 line 385
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2102 line 433
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2103 line 438
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2103 line 483
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2104 line 488
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2104 line 533
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2105 line 538
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2105 line 571
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2106 line 576
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2106 line 594
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2107 line 599
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2107 line 632
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2108 line 637
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2108 line 670
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2109 line 675
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2109 line 744
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2110 line 749
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2110 line 818
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero2111 line 823
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound2111 line 856
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2096 line 861
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2097 line 864
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2098 line 867
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2099 line 870
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2100 line 873
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2101 line 876
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2102 line 879
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2103 line 882
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2104 line 885
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2105 line 888
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2106 line 891
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2107 line 894
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2108 line 897
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2109 line 900
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2110 line 903
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt2111 line 906
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound131 line 909