OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical70.lean

GitHub source file

91 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2240 line 13
  2. def OAI.MUB6.Certificate.PairSemantics.raw2240step0 line 15
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical2240 line 17
  4. def OAI.MUB6.Certificate.PairSemantics.raw2241 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw2241step0 line 28
  6. def OAI.MUB6.Certificate.PairSemantics.raw2241step1 line 30
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical2241 line 32
  8. def OAI.MUB6.Certificate.PairSemantics.raw2242 line 46
  9. def OAI.MUB6.Certificate.PairSemantics.raw2242step0 line 48
  10. def OAI.MUB6.Certificate.PairSemantics.raw2242step1 line 50
  11. def OAI.MUB6.Certificate.PairSemantics.raw2242step2 line 52
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical2242 line 54
  13. def OAI.MUB6.Certificate.PairSemantics.raw2243 line 72
  14. def OAI.MUB6.Certificate.PairSemantics.raw2243step0 line 74
  15. def OAI.MUB6.Certificate.PairSemantics.raw2243step1 line 76
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical2243 line 78
  17. def OAI.MUB6.Certificate.PairSemantics.raw2244 line 92
  18. def OAI.MUB6.Certificate.PairSemantics.raw2244step0 line 94
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical2244 line 96
  20. def OAI.MUB6.Certificate.PairSemantics.raw2245 line 105
  21. def OAI.MUB6.Certificate.PairSemantics.raw2245step0 line 107
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical2245 line 109
  23. def OAI.MUB6.Certificate.PairSemantics.raw2246 line 118
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical2246 line 120
  25. def OAI.MUB6.Certificate.PairSemantics.raw2247 line 124
  26. def OAI.MUB6.Certificate.PairSemantics.raw2247step0 line 126
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical2247 line 128
  28. def OAI.MUB6.Certificate.PairSemantics.raw2248 line 137
  29. def OAI.MUB6.Certificate.PairSemantics.raw2248step0 line 139
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical2248 line 141
  31. def OAI.MUB6.Certificate.PairSemantics.raw2249 line 150
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical2249 line 152
  33. def OAI.MUB6.Certificate.PairSemantics.raw2250 line 156
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical2250 line 158
  35. def OAI.MUB6.Certificate.PairSemantics.raw2251 line 162
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical2251 line 164
  37. def OAI.MUB6.Certificate.PairSemantics.raw2252 line 168
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical2252 line 170
  39. def OAI.MUB6.Certificate.PairSemantics.raw2253 line 174
  40. def OAI.MUB6.Certificate.PairSemantics.raw2253step0 line 176
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical2253 line 178
  42. def OAI.MUB6.Certificate.PairSemantics.raw2254 line 187
  43. def OAI.MUB6.Certificate.PairSemantics.raw2254step0 line 189
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical2254 line 191
  45. def OAI.MUB6.Certificate.PairSemantics.raw2255 line 200
  46. def OAI.MUB6.Certificate.PairSemantics.raw2255step0 line 202
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical2255 line 204
  48. def OAI.MUB6.Certificate.PairSemantics.raw2256 line 213
  49. def OAI.MUB6.Certificate.PairSemantics.raw2256step0 line 215
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical2256 line 217
  51. def OAI.MUB6.Certificate.PairSemantics.raw2257 line 226
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical2257 line 228
  53. def OAI.MUB6.Certificate.PairSemantics.raw2258 line 232
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical2258 line 234
  55. def OAI.MUB6.Certificate.PairSemantics.raw2259 line 238
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical2259 line 240
  57. def OAI.MUB6.Certificate.PairSemantics.raw2260 line 244
  58. def OAI.MUB6.Certificate.PairSemantics.raw2260step0 line 246
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical2260 line 248
  60. def OAI.MUB6.Certificate.PairSemantics.raw2261 line 257
  61. def OAI.MUB6.Certificate.PairSemantics.raw2261step0 line 259
  62. def OAI.MUB6.Certificate.PairSemantics.raw2261step1 line 261
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical2261 line 263
  64. def OAI.MUB6.Certificate.PairSemantics.raw2262 line 276
  65. def OAI.MUB6.Certificate.PairSemantics.raw2262step0 line 278
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical2262 line 280
  67. def OAI.MUB6.Certificate.PairSemantics.raw2263 line 289
  68. def OAI.MUB6.Certificate.PairSemantics.raw2263step0 line 291
  69. def OAI.MUB6.Certificate.PairSemantics.raw2263step1 line 293
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical2263 line 295
  71. def OAI.MUB6.Certificate.PairSemantics.raw2264 line 308
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical2264 line 310
  73. def OAI.MUB6.Certificate.PairSemantics.raw2265 line 314
  74. def OAI.MUB6.Certificate.PairSemantics.raw2265step0 line 316
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical2265 line 318
  76. def OAI.MUB6.Certificate.PairSemantics.raw2266 line 327
  77. def OAI.MUB6.Certificate.PairSemantics.raw2266step0 line 329
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical2266 line 331
  79. def OAI.MUB6.Certificate.PairSemantics.raw2267 line 340
  80. def OAI.MUB6.Certificate.PairSemantics.raw2267step0 line 342
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical2267 line 344
  82. def OAI.MUB6.Certificate.PairSemantics.raw2268 line 353
  83. def OAI.MUB6.Certificate.PairSemantics.raw2268step0 line 355
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical2268 line 357
  85. def OAI.MUB6.Certificate.PairSemantics.raw2269 line 366
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical2269 line 368
  87. def OAI.MUB6.Certificate.PairSemantics.raw2270 line 372
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical2270 line 374
  89. def OAI.MUB6.Certificate.PairSemantics.raw2271 line 378
  90. def OAI.MUB6.Certificate.PairSemantics.raw2271step0 line 380
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical2271 line 382