OAI/Analysis/MutuallyUnbiased/MixedSources/Rows92.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1472 line 49
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1472 line 139
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1473 line 144
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1473 line 234
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1474 line 239
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1474 line 266
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1475 line 271
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1475 line 295
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1476 line 300
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1476 line 327
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1477 line 332
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1477 line 425
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1478 line 430
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1478 line 523
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1479 line 528
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1479 line 621
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1480 line 626
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1480 line 719
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1481 line 724
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1481 line 751
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1482 line 756
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1482 line 783
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1483 line 788
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1483 line 857
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1484 line 862
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1484 line 931
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1485 line 936
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1485 line 1005
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1486 line 1010
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1486 line 1034
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1487 line 1039
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1487 line 1063
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1472 line 1068
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1473 line 1071
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1474 line 1074
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1475 line 1077
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1476 line 1080
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1477 line 1083
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1478 line 1086
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1479 line 1089
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1480 line 1092
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1481 line 1095
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1482 line 1098
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1483 line 1101
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1484 line 1104
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1485 line 1107
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1486 line 1110
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1487 line 1113
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound92 line 1116