OAI/Analysis/MutuallyUnbiased/MixedSources/Rows123.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1968 line 59
  2. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1968 line 152
  3. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1969 line 157
  4. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1969 line 250
  5. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1970 line 255
  6. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1970 line 351
  7. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1971 line 356
  8. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1971 line 425
  9. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1972 line 430
  10. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1972 line 499
  11. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1973 line 504
  12. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1973 line 573
  13. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1974 line 578
  14. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1974 line 602
  15. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1975 line 607
  16. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1975 line 628
  17. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1976 line 633
  18. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1976 line 702
  19. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1977 line 707
  20. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1977 line 776
  21. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1978 line 781
  22. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1978 line 850
  23. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1979 line 855
  24. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1979 line 879
  25. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1980 line 884
  26. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1980 line 953
  27. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1981 line 958
  28. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1981 line 1027
  29. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1982 line 1032
  30. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1982 line 1056
  31. theorem OAI.MUB6.Certificate.MixedSourceBridge.reducedZero1983 line 1061
  32. theorem OAI.MUB6.Certificate.MixedSourceBridge.rowSound1983 line 1130
  33. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1968 line 1135
  34. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1969 line 1138
  35. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1970 line 1141
  36. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1971 line 1144
  37. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1972 line 1147
  38. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1973 line 1150
  39. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1974 line 1153
  40. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1975 line 1156
  41. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1976 line 1159
  42. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1977 line 1162
  43. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1978 line 1165
  44. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1979 line 1168
  45. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1980 line 1171
  46. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1981 line 1174
  47. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1982 line 1177
  48. theorem OAI.MUB6.Certificate.MixedSourceBridge.sourceRowsAt1983 line 1180
  49. theorem OAI.MUB6.Certificate.MixedSourceBridge.chunkSound123 line 1183