OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sound31.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MUB6.Certificate.MixedSemantics.sound1984 line 10
  2. theorem OAI.MUB6.Certificate.MixedSemantics.sound1985 line 16
  3. theorem OAI.MUB6.Certificate.MixedSemantics.sound1986 line 22
  4. theorem OAI.MUB6.Certificate.MixedSemantics.sound1987 line 28
  5. theorem OAI.MUB6.Certificate.MixedSemantics.sound1988 line 34
  6. theorem OAI.MUB6.Certificate.MixedSemantics.sound1989 line 40
  7. theorem OAI.MUB6.Certificate.MixedSemantics.sound1990 line 46
  8. theorem OAI.MUB6.Certificate.MixedSemantics.sound1991 line 52
  9. theorem OAI.MUB6.Certificate.MixedSemantics.sound1992 line 58
  10. theorem OAI.MUB6.Certificate.MixedSemantics.sound1993 line 64
  11. theorem OAI.MUB6.Certificate.MixedSemantics.sound1994 line 70
  12. theorem OAI.MUB6.Certificate.MixedSemantics.sound1995 line 76
  13. theorem OAI.MUB6.Certificate.MixedSemantics.sound1996 line 82
  14. theorem OAI.MUB6.Certificate.MixedSemantics.sound1997 line 88
  15. theorem OAI.MUB6.Certificate.MixedSemantics.sound1998 line 94
  16. theorem OAI.MUB6.Certificate.MixedSemantics.sound1999 line 100
  17. theorem OAI.MUB6.Certificate.MixedSemantics.sound2000 line 105
  18. theorem OAI.MUB6.Certificate.MixedSemantics.sound2001 line 111
  19. theorem OAI.MUB6.Certificate.MixedSemantics.sound2002 line 117
  20. theorem OAI.MUB6.Certificate.MixedSemantics.sound2003 line 123
  21. theorem OAI.MUB6.Certificate.MixedSemantics.sound2004 line 129
  22. theorem OAI.MUB6.Certificate.MixedSemantics.sound2005 line 135
  23. theorem OAI.MUB6.Certificate.MixedSemantics.sound2006 line 141
  24. theorem OAI.MUB6.Certificate.MixedSemantics.sound2007 line 147
  25. theorem OAI.MUB6.Certificate.MixedSemantics.sound2008 line 152
  26. theorem OAI.MUB6.Certificate.MixedSemantics.sound2009 line 158
  27. theorem OAI.MUB6.Certificate.MixedSemantics.sound2010 line 164
  28. theorem OAI.MUB6.Certificate.MixedSemantics.sound2011 line 170
  29. theorem OAI.MUB6.Certificate.MixedSemantics.sound2012 line 176
  30. theorem OAI.MUB6.Certificate.MixedSemantics.sound2013 line 182
  31. theorem OAI.MUB6.Certificate.MixedSemantics.sound2014 line 188
  32. theorem OAI.MUB6.Certificate.MixedSemantics.sound2015 line 194
  33. theorem OAI.MUB6.Certificate.MixedSemantics.sound2016 line 200
  34. theorem OAI.MUB6.Certificate.MixedSemantics.sound2017 line 206
  35. theorem OAI.MUB6.Certificate.MixedSemantics.sound2018 line 212
  36. theorem OAI.MUB6.Certificate.MixedSemantics.sound2019 line 218
  37. theorem OAI.MUB6.Certificate.MixedSemantics.sound2020 line 224
  38. theorem OAI.MUB6.Certificate.MixedSemantics.sound2021 line 230
  39. theorem OAI.MUB6.Certificate.MixedSemantics.sound2022 line 236
  40. theorem OAI.MUB6.Certificate.MixedSemantics.sound2023 line 242
  41. theorem OAI.MUB6.Certificate.MixedSemantics.sound2024 line 248
  42. theorem OAI.MUB6.Certificate.MixedSemantics.sound2025 line 254
  43. theorem OAI.MUB6.Certificate.MixedSemantics.sound2026 line 260
  44. theorem OAI.MUB6.Certificate.MixedSemantics.sound2027 line 266
  45. theorem OAI.MUB6.Certificate.MixedSemantics.sound2028 line 272
  46. theorem OAI.MUB6.Certificate.MixedSemantics.sound2029 line 278
  47. theorem OAI.MUB6.Certificate.MixedSemantics.sound2030 line 284
  48. theorem OAI.MUB6.Certificate.MixedSemantics.sound2031 line 290
  49. theorem OAI.MUB6.Certificate.MixedSemantics.sound2032 line 296
  50. theorem OAI.MUB6.Certificate.MixedSemantics.sound2033 line 302
  51. theorem OAI.MUB6.Certificate.MixedSemantics.sound2034 line 308
  52. theorem OAI.MUB6.Certificate.MixedSemantics.sound2035 line 314
  53. theorem OAI.MUB6.Certificate.MixedSemantics.sound2036 line 320
  54. theorem OAI.MUB6.Certificate.MixedSemantics.sound2037 line 326
  55. theorem OAI.MUB6.Certificate.MixedSemantics.sound2038 line 332
  56. theorem OAI.MUB6.Certificate.MixedSemantics.sound2039 line 338
  57. theorem OAI.MUB6.Certificate.MixedSemantics.sound2040 line 344
  58. theorem OAI.MUB6.Certificate.MixedSemantics.sound2041 line 350
  59. theorem OAI.MUB6.Certificate.MixedSemantics.sound2042 line 356
  60. theorem OAI.MUB6.Certificate.MixedSemantics.sound2043 line 362
  61. theorem OAI.MUB6.Certificate.MixedSemantics.sound2044 line 368
  62. theorem OAI.MUB6.Certificate.MixedSemantics.sound2045 line 374
  63. theorem OAI.MUB6.Certificate.MixedSemantics.sound2046 line 380
  64. theorem OAI.MUB6.Certificate.MixedSemantics.sound2047 line 386