OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical61.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1952 line 12
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical1952 line 14
  3. def OAI.MUB6.Certificate.PairSemantics.raw1953 line 18
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical1953 line 20
  5. def OAI.MUB6.Certificate.PairSemantics.raw1954 line 24
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical1954 line 26
  7. def OAI.MUB6.Certificate.PairSemantics.raw1955 line 30
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical1955 line 32
  9. def OAI.MUB6.Certificate.PairSemantics.raw1956 line 36
  10. def OAI.MUB6.Certificate.PairSemantics.raw1956step0 line 38
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical1956 line 40
  12. def OAI.MUB6.Certificate.PairSemantics.raw1957 line 49
  13. def OAI.MUB6.Certificate.PairSemantics.raw1957step0 line 51
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical1957 line 53
  15. def OAI.MUB6.Certificate.PairSemantics.raw1958 line 62
  16. def OAI.MUB6.Certificate.PairSemantics.raw1958step0 line 64
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical1958 line 66
  18. def OAI.MUB6.Certificate.PairSemantics.raw1959 line 75
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical1959 line 77
  20. def OAI.MUB6.Certificate.PairSemantics.raw1960 line 81
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical1960 line 83
  22. def OAI.MUB6.Certificate.PairSemantics.raw1961 line 87
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical1961 line 89
  24. def OAI.MUB6.Certificate.PairSemantics.raw1962 line 93
  25. def OAI.MUB6.Certificate.PairSemantics.raw1962step0 line 95
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical1962 line 97
  27. def OAI.MUB6.Certificate.PairSemantics.raw1963 line 106
  28. def OAI.MUB6.Certificate.PairSemantics.raw1963step0 line 108
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical1963 line 110
  30. def OAI.MUB6.Certificate.PairSemantics.raw1964 line 119
  31. def OAI.MUB6.Certificate.PairSemantics.raw1964step0 line 121
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical1964 line 123
  33. def OAI.MUB6.Certificate.PairSemantics.raw1965 line 132
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical1965 line 134
  35. def OAI.MUB6.Certificate.PairSemantics.raw1966 line 138
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical1966 line 140
  37. def OAI.MUB6.Certificate.PairSemantics.raw1967 line 144
  38. def OAI.MUB6.Certificate.PairSemantics.raw1967step0 line 146
  39. def OAI.MUB6.Certificate.PairSemantics.raw1967step1 line 148
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical1967 line 150
  41. def OAI.MUB6.Certificate.PairSemantics.raw1968 line 163
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical1968 line 165
  43. def OAI.MUB6.Certificate.PairSemantics.raw1969 line 169
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical1969 line 171
  45. def OAI.MUB6.Certificate.PairSemantics.raw1970 line 175
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical1970 line 177
  47. def OAI.MUB6.Certificate.PairSemantics.raw1971 line 181
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical1971 line 183
  49. def OAI.MUB6.Certificate.PairSemantics.raw1972 line 187
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical1972 line 189
  51. def OAI.MUB6.Certificate.PairSemantics.raw1973 line 193
  52. def OAI.MUB6.Certificate.PairSemantics.raw1973step0 line 195
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical1973 line 197
  54. def OAI.MUB6.Certificate.PairSemantics.raw1974 line 206
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical1974 line 208
  56. def OAI.MUB6.Certificate.PairSemantics.raw1975 line 212
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical1975 line 214
  58. def OAI.MUB6.Certificate.PairSemantics.raw1976 line 218
  59. def OAI.MUB6.Certificate.PairSemantics.raw1976step0 line 220
  60. def OAI.MUB6.Certificate.PairSemantics.raw1976step1 line 222
  61. def OAI.MUB6.Certificate.PairSemantics.raw1976step2 line 224
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical1976 line 226
  63. def OAI.MUB6.Certificate.PairSemantics.raw1977 line 243
  64. def OAI.MUB6.Certificate.PairSemantics.raw1977step0 line 245
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical1977 line 247
  66. def OAI.MUB6.Certificate.PairSemantics.raw1978 line 256
  67. def OAI.MUB6.Certificate.PairSemantics.raw1978step0 line 258
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical1978 line 260
  69. def OAI.MUB6.Certificate.PairSemantics.raw1979 line 269
  70. def OAI.MUB6.Certificate.PairSemantics.raw1979step0 line 271
  71. def OAI.MUB6.Certificate.PairSemantics.raw1979step1 line 273
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical1979 line 275
  73. def OAI.MUB6.Certificate.PairSemantics.raw1980 line 288
  74. def OAI.MUB6.Certificate.PairSemantics.raw1980step0 line 290
  75. def OAI.MUB6.Certificate.PairSemantics.raw1980step1 line 292
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical1980 line 294
  77. def OAI.MUB6.Certificate.PairSemantics.raw1981 line 307
  78. def OAI.MUB6.Certificate.PairSemantics.raw1981step0 line 309
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical1981 line 311
  80. def OAI.MUB6.Certificate.PairSemantics.raw1982 line 320
  81. def OAI.MUB6.Certificate.PairSemantics.raw1982step0 line 322
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical1982 line 324
  83. def OAI.MUB6.Certificate.PairSemantics.raw1983 line 333
  84. def OAI.MUB6.Certificate.PairSemantics.raw1983step0 line 335
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical1983 line 337