OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sound30.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSemantics.sound1920 line 10
  2. theorem OAI.MUB6.Certificate.MixedSemantics.sound1921 line 16
  3. theorem OAI.MUB6.Certificate.MixedSemantics.sound1922 line 22
  4. theorem OAI.MUB6.Certificate.MixedSemantics.sound1923 line 28
  5. theorem OAI.MUB6.Certificate.MixedSemantics.sound1924 line 34
  6. theorem OAI.MUB6.Certificate.MixedSemantics.sound1925 line 40
  7. theorem OAI.MUB6.Certificate.MixedSemantics.sound1926 line 46
  8. theorem OAI.MUB6.Certificate.MixedSemantics.sound1927 line 52
  9. theorem OAI.MUB6.Certificate.MixedSemantics.sound1928 line 58
  10. theorem OAI.MUB6.Certificate.MixedSemantics.sound1929 line 64
  11. theorem OAI.MUB6.Certificate.MixedSemantics.sound1930 line 70
  12. theorem OAI.MUB6.Certificate.MixedSemantics.sound1931 line 76
  13. theorem OAI.MUB6.Certificate.MixedSemantics.sound1932 line 82
  14. theorem OAI.MUB6.Certificate.MixedSemantics.sound1933 line 88
  15. theorem OAI.MUB6.Certificate.MixedSemantics.sound1934 line 94
  16. theorem OAI.MUB6.Certificate.MixedSemantics.sound1935 line 100
  17. theorem OAI.MUB6.Certificate.MixedSemantics.sound1936 line 106
  18. theorem OAI.MUB6.Certificate.MixedSemantics.sound1937 line 112
  19. theorem OAI.MUB6.Certificate.MixedSemantics.sound1938 line 118
  20. theorem OAI.MUB6.Certificate.MixedSemantics.sound1939 line 124
  21. theorem OAI.MUB6.Certificate.MixedSemantics.sound1940 line 130
  22. theorem OAI.MUB6.Certificate.MixedSemantics.sound1941 line 136
  23. theorem OAI.MUB6.Certificate.MixedSemantics.sound1942 line 142
  24. theorem OAI.MUB6.Certificate.MixedSemantics.sound1943 line 148
  25. theorem OAI.MUB6.Certificate.MixedSemantics.sound1944 line 153
  26. theorem OAI.MUB6.Certificate.MixedSemantics.sound1945 line 158
  27. theorem OAI.MUB6.Certificate.MixedSemantics.sound1946 line 163
  28. theorem OAI.MUB6.Certificate.MixedSemantics.sound1947 line 169
  29. theorem OAI.MUB6.Certificate.MixedSemantics.sound1948 line 174
  30. theorem OAI.MUB6.Certificate.MixedSemantics.sound1949 line 180
  31. theorem OAI.MUB6.Certificate.MixedSemantics.sound1950 line 186
  32. theorem OAI.MUB6.Certificate.MixedSemantics.sound1951 line 191
  33. theorem OAI.MUB6.Certificate.MixedSemantics.sound1952 line 197
  34. theorem OAI.MUB6.Certificate.MixedSemantics.sound1953 line 203
  35. theorem OAI.MUB6.Certificate.MixedSemantics.sound1954 line 208
  36. theorem OAI.MUB6.Certificate.MixedSemantics.sound1955 line 214
  37. theorem OAI.MUB6.Certificate.MixedSemantics.sound1956 line 220
  38. theorem OAI.MUB6.Certificate.MixedSemantics.sound1957 line 226
  39. theorem OAI.MUB6.Certificate.MixedSemantics.sound1958 line 232
  40. theorem OAI.MUB6.Certificate.MixedSemantics.sound1959 line 238
  41. theorem OAI.MUB6.Certificate.MixedSemantics.sound1960 line 244
  42. theorem OAI.MUB6.Certificate.MixedSemantics.sound1961 line 250
  43. theorem OAI.MUB6.Certificate.MixedSemantics.sound1962 line 256
  44. theorem OAI.MUB6.Certificate.MixedSemantics.sound1963 line 262
  45. theorem OAI.MUB6.Certificate.MixedSemantics.sound1964 line 268
  46. theorem OAI.MUB6.Certificate.MixedSemantics.sound1965 line 274
  47. theorem OAI.MUB6.Certificate.MixedSemantics.sound1966 line 280
  48. theorem OAI.MUB6.Certificate.MixedSemantics.sound1967 line 286
  49. theorem OAI.MUB6.Certificate.MixedSemantics.sound1968 line 292
  50. theorem OAI.MUB6.Certificate.MixedSemantics.sound1969 line 298
  51. theorem OAI.MUB6.Certificate.MixedSemantics.sound1970 line 304
  52. theorem OAI.MUB6.Certificate.MixedSemantics.sound1971 line 310
  53. theorem OAI.MUB6.Certificate.MixedSemantics.sound1972 line 316
  54. theorem OAI.MUB6.Certificate.MixedSemantics.sound1973 line 322
  55. theorem OAI.MUB6.Certificate.MixedSemantics.sound1974 line 328
  56. theorem OAI.MUB6.Certificate.MixedSemantics.sound1975 line 334
  57. theorem OAI.MUB6.Certificate.MixedSemantics.sound1976 line 340
  58. theorem OAI.MUB6.Certificate.MixedSemantics.sound1977 line 346
  59. theorem OAI.MUB6.Certificate.MixedSemantics.sound1978 line 352
  60. theorem OAI.MUB6.Certificate.MixedSemantics.sound1979 line 358
  61. theorem OAI.MUB6.Certificate.MixedSemantics.sound1980 line 364
  62. theorem OAI.MUB6.Certificate.MixedSemantics.sound1981 line 370
  63. theorem OAI.MUB6.Certificate.MixedSemantics.sound1982 line 376
  64. theorem OAI.MUB6.Certificate.MixedSemantics.sound1983 line 382