OAI/Analysis/MutuallyUnbiased/MixedSources/Rows98.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1568 line 48
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1568 line 96
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1569 line 101
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1569 line 131
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1570 line 136
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1570 line 160
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1571 line 165
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1571 line 210
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1572 line 215
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1572 line 260
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1573 line 265
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1573 line 310
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1574 line 315
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1574 line 336
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1575 line 341
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1575 line 386
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1576 line 391
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1576 line 436
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1577 line 441
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1577 line 465
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1578 line 470
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1578 line 488
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1579 line 493
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1579 line 511
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1580 line 516
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1580 line 540
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1581 line 545
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1581 line 572
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1582 line 577
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1582 line 598
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1583 line 603
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1583 line 624
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1568 line 629
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1569 line 632
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1570 line 635
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1571 line 638
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1572 line 641
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1573 line 644
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1574 line 647
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1575 line 650
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1576 line 653
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1577 line 656
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1578 line 659
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1579 line 662
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1580 line 665
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1581 line 668
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1582 line 671
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1583 line 674
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound98 line 677