OAI/Analysis/MutuallyUnbiased/MixedSources/Rows93.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1488 line 48
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1488 line 72
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1489 line 77
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1489 line 98
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1490 line 103
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1490 line 172
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1491 line 177
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1491 line 246
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1492 line 251
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1492 line 320
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1493 line 325
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1493 line 394
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1494 line 399
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1494 line 426
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1495 line 431
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1495 line 458
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1496 line 463
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1496 line 490
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1497 line 495
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1497 line 522
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1498 line 527
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1498 line 551
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1499 line 556
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1499 line 577
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1500 line 582
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1500 line 609
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1501 line 614
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1501 line 641
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1502 line 646
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1502 line 673
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1503 line 678
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1503 line 702
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1488 line 707
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1489 line 710
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1490 line 713
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1491 line 716
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1492 line 719
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1493 line 722
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1494 line 725
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1495 line 728
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1496 line 731
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1497 line 734
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1498 line 737
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1499 line 740
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1500 line 743
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1501 line 746
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1502 line 749
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1503 line 752
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound93 line 755