OAI/Analysis/MutuallyUnbiased/MixedSources/Rows97.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1552 line 38
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1552 line 62
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1553 line 67
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1553 line 91
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1554 line 96
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1554 line 120
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1555 line 125
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1555 line 149
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1556 line 154
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1556 line 175
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1557 line 180
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1557 line 204
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1558 line 209
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1558 line 236
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1559 line 241
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1559 line 286
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1560 line 291
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1560 line 336
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1561 line 341
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1561 line 386
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1562 line 391
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1562 line 436
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1563 line 441
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1563 line 486
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1564 line 491
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1564 line 512
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1565 line 517
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1565 line 562
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1566 line 567
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1566 line 588
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1567 line 593
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1567 line 641
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1552 line 646
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1553 line 649
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1554 line 652
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1555 line 655
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1556 line 658
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1557 line 661
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1558 line 664
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1559 line 667
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1560 line 670
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1561 line 673
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1562 line 676
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1563 line 679
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1564 line 682
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1565 line 685
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1566 line 688
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1567 line 691
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound97 line 694