OAI/Analysis/MutuallyUnbiased/MixedSources/Rows99.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1584 line 41
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1584 line 89
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1585 line 94
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1585 line 142
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1586 line 147
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1586 line 165
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1587 line 170
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1587 line 218
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1588 line 223
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1588 line 271
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1589 line 276
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1589 line 324
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1590 line 329
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1590 line 356
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1591 line 361
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1591 line 385
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1592 line 390
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1592 line 414
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1593 line 419
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1593 line 488
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1594 line 493
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1594 line 562
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1595 line 567
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1595 line 612
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1596 line 617
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1596 line 641
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1597 line 646
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1597 line 667
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1598 line 672
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1598 line 699
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1599 line 704
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1599 line 749
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1584 line 754
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1585 line 757
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1586 line 760
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1587 line 763
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1588 line 766
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1589 line 769
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1590 line 772
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1591 line 775
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1592 line 778
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1593 line 781
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1594 line 784
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1595 line 787
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1596 line 790
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1597 line 793
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1598 line 796
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1599 line 799
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound99 line 802