OAI/Analysis/MutuallyUnbiased/MixedSources/Rows61.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero976 line 35
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound976 line 92
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero977 line 97
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound977 line 160
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero978 line 165
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound978 line 225
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero979 line 230
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound979 line 272
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero980 line 277
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound980 line 343
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero981 line 348
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound981 line 417
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero982 line 422
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound982 line 461
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero983 line 466
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound983 line 514
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero984 line 519
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound984 line 588
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero985 line 593
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound985 line 662
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero986 line 667
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound986 line 736
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero987 line 741
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound987 line 810
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero988 line 815
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound988 line 881
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero989 line 886
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound989 line 952
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero990 line 957
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound990 line 1002
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero991 line 1007
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound991 line 1046
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt976 line 1051
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt977 line 1054
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt978 line 1057
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt979 line 1060
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt980 line 1063
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt981 line 1066
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt982 line 1069
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt983 line 1072
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt984 line 1075
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt985 line 1078
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt986 line 1081
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt987 line 1084
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt988 line 1087
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt989 line 1090
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt990 line 1093
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt991 line 1096
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound61 line 1099