OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical67.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2144 line 17
  2. def OAI.MUB6.Certificate.PairSemantics.raw2144step0 line 19
  3. def OAI.MUB6.Certificate.PairSemantics.raw2144step1 line 21
  4. def OAI.MUB6.Certificate.PairSemantics.raw2144step2 line 23
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical2144 line 25
  6. def OAI.MUB6.Certificate.PairSemantics.raw2145 line 42
  7. def OAI.MUB6.Certificate.PairSemantics.raw2145step0 line 44
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical2145 line 46
  9. def OAI.MUB6.Certificate.PairSemantics.raw2146 line 55
  10. def OAI.MUB6.Certificate.PairSemantics.raw2146step0 line 57
  11. def OAI.MUB6.Certificate.PairSemantics.raw2146step1 line 59
  12. def OAI.MUB6.Certificate.PairSemantics.raw2146step2 line 61
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical2146 line 63
  14. def OAI.MUB6.Certificate.PairSemantics.raw2147 line 80
  15. def OAI.MUB6.Certificate.PairSemantics.raw2147step0 line 82
  16. def OAI.MUB6.Certificate.PairSemantics.raw2147step1 line 84
  17. def OAI.MUB6.Certificate.PairSemantics.raw2147step2 line 86
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical2147 line 88
  19. def OAI.MUB6.Certificate.PairSemantics.raw2148 line 105
  20. def OAI.MUB6.Certificate.PairSemantics.raw2148step0 line 107
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical2148 line 109
  22. def OAI.MUB6.Certificate.PairSemantics.raw2149 line 118
  23. def OAI.MUB6.Certificate.PairSemantics.raw2149step0 line 120
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical2149 line 122
  25. def OAI.MUB6.Certificate.PairSemantics.raw2150 line 131
  26. def OAI.MUB6.Certificate.PairSemantics.raw2150step0 line 133
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical2150 line 135
  28. def OAI.MUB6.Certificate.PairSemantics.raw2151 line 144
  29. def OAI.MUB6.Certificate.PairSemantics.raw2151step0 line 146
  30. def OAI.MUB6.Certificate.PairSemantics.raw2151step1 line 148
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical2151 line 150
  32. def OAI.MUB6.Certificate.PairSemantics.raw2152 line 163
  33. def OAI.MUB6.Certificate.PairSemantics.raw2152step0 line 165
  34. def OAI.MUB6.Certificate.PairSemantics.raw2152step1 line 167
  35. def OAI.MUB6.Certificate.PairSemantics.raw2152step2 line 169
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical2152 line 171
  37. def OAI.MUB6.Certificate.PairSemantics.raw2153 line 188
  38. def OAI.MUB6.Certificate.PairSemantics.raw2153step0 line 190
  39. def OAI.MUB6.Certificate.PairSemantics.raw2153step1 line 192
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical2153 line 194
  41. def OAI.MUB6.Certificate.PairSemantics.raw2154 line 207
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical2154 line 209
  43. def OAI.MUB6.Certificate.PairSemantics.raw2155 line 213
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical2155 line 215
  45. def OAI.MUB6.Certificate.PairSemantics.raw2156 line 219
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical2156 line 221
  47. def OAI.MUB6.Certificate.PairSemantics.raw2157 line 225
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical2157 line 227
  49. def OAI.MUB6.Certificate.PairSemantics.raw2158 line 231
  50. def OAI.MUB6.Certificate.PairSemantics.raw2158step0 line 233
  51. def OAI.MUB6.Certificate.PairSemantics.raw2158step1 line 235
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical2158 line 237
  53. def OAI.MUB6.Certificate.PairSemantics.raw2159 line 250
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical2159 line 252
  55. def OAI.MUB6.Certificate.PairSemantics.raw2160 line 256
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical2160 line 258
  57. def OAI.MUB6.Certificate.PairSemantics.raw2161 line 262
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical2161 line 264
  59. def OAI.MUB6.Certificate.PairSemantics.raw2162 line 268
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical2162 line 270
  61. def OAI.MUB6.Certificate.PairSemantics.raw2163 line 274
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical2163 line 276
  63. def OAI.MUB6.Certificate.PairSemantics.raw2164 line 280
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical2164 line 282
  65. def OAI.MUB6.Certificate.PairSemantics.raw2165 line 286
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical2165 line 288
  67. def OAI.MUB6.Certificate.PairSemantics.raw2166 line 292
  68. def OAI.MUB6.Certificate.PairSemantics.raw2166step0 line 294
  69. def OAI.MUB6.Certificate.PairSemantics.raw2166step1 line 296
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical2166 line 298
  71. def OAI.MUB6.Certificate.PairSemantics.raw2167 line 311
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical2167 line 313
  73. def OAI.MUB6.Certificate.PairSemantics.raw2168 line 317
  74. def OAI.MUB6.Certificate.PairSemantics.raw2168step0 line 319
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical2168 line 321
  76. def OAI.MUB6.Certificate.PairSemantics.raw2169 line 330
  77. def OAI.MUB6.Certificate.PairSemantics.raw2169step0 line 332
  78. def OAI.MUB6.Certificate.PairSemantics.raw2169step1 line 334
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical2169 line 336
  80. def OAI.MUB6.Certificate.PairSemantics.raw2170 line 349
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical2170 line 351
  82. def OAI.MUB6.Certificate.PairSemantics.raw2171 line 355
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical2171 line 357
  84. def OAI.MUB6.Certificate.PairSemantics.raw2172 line 361
  85. def OAI.MUB6.Certificate.PairSemantics.raw2172step0 line 363
  86. def OAI.MUB6.Certificate.PairSemantics.raw2172step1 line 365
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical2172 line 367
  88. def OAI.MUB6.Certificate.PairSemantics.raw2173 line 380
  89. def OAI.MUB6.Certificate.PairSemantics.raw2173step0 line 382
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical2173 line 384
  91. def OAI.MUB6.Certificate.PairSemantics.raw2174 line 393
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical2174 line 395
  93. def OAI.MUB6.Certificate.PairSemantics.raw2175 line 399
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical2175 line 401