OAI/Analysis/MutuallyUnbiased/MixedSources/Rows122.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1952 line 56
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1952 line 149
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1953 line 154
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1953 line 247
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1954 line 252
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1954 line 345
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1955 line 350
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1955 line 377
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1956 line 382
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1956 line 451
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1957 line 456
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1957 line 525
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1958 line 530
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1958 line 599
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1959 line 604
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1959 line 673
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1960 line 678
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1960 line 747
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1961 line 752
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1961 line 821
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1962 line 826
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1962 line 850
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1963 line 855
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1963 line 921
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1964 line 926
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1964 line 995
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1965 line 1000
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1965 line 1093
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1966 line 1098
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1966 line 1191
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1967 line 1196
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1967 line 1223
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1952 line 1228
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1953 line 1231
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1954 line 1234
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1955 line 1237
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1956 line 1240
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1957 line 1243
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1958 line 1246
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1959 line 1249
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1960 line 1252
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1961 line 1255
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1962 line 1258
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1963 line 1261
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1964 line 1264
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1965 line 1267
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1966 line 1270
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1967 line 1273
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound122 line 1276