OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical99.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3168 line 13
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical3168 line 15
  3. def OAI.MUB6.Certificate.PairSemantics.raw3169 line 19
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical3169 line 21
  5. def OAI.MUB6.Certificate.PairSemantics.raw3170 line 25
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical3170 line 27
  7. def OAI.MUB6.Certificate.PairSemantics.raw3171 line 31
  8. def OAI.MUB6.Certificate.PairSemantics.raw3171step0 line 33
  9. def OAI.MUB6.Certificate.PairSemantics.raw3171step1 line 35
  10. def OAI.MUB6.Certificate.PairSemantics.raw3171step2 line 37
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical3171 line 39
  12. def OAI.MUB6.Certificate.PairSemantics.raw3172 line 56
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical3172 line 58
  14. def OAI.MUB6.Certificate.PairSemantics.raw3173 line 62
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical3173 line 64
  16. def OAI.MUB6.Certificate.PairSemantics.raw3174 line 68
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical3174 line 70
  18. def OAI.MUB6.Certificate.PairSemantics.raw3175 line 74
  19. def OAI.MUB6.Certificate.PairSemantics.raw3175step0 line 76
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical3175 line 78
  21. def OAI.MUB6.Certificate.PairSemantics.raw3176 line 87
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical3176 line 89
  23. def OAI.MUB6.Certificate.PairSemantics.raw3177 line 93
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical3177 line 95
  25. def OAI.MUB6.Certificate.PairSemantics.raw3178 line 99
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical3178 line 101
  27. def OAI.MUB6.Certificate.PairSemantics.raw3179 line 105
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical3179 line 107
  29. def OAI.MUB6.Certificate.PairSemantics.raw3180 line 111
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical3180 line 113
  31. def OAI.MUB6.Certificate.PairSemantics.raw3181 line 117
  32. def OAI.MUB6.Certificate.PairSemantics.raw3181step0 line 119
  33. def OAI.MUB6.Certificate.PairSemantics.raw3181step1 line 121
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical3181 line 123
  35. def OAI.MUB6.Certificate.PairSemantics.raw3182 line 136
  36. def OAI.MUB6.Certificate.PairSemantics.raw3182step0 line 138
  37. def OAI.MUB6.Certificate.PairSemantics.raw3182step1 line 140
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical3182 line 142
  39. def OAI.MUB6.Certificate.PairSemantics.raw3183 line 155
  40. def OAI.MUB6.Certificate.PairSemantics.raw3183step0 line 157
  41. def OAI.MUB6.Certificate.PairSemantics.raw3183step1 line 159
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical3183 line 161
  43. def OAI.MUB6.Certificate.PairSemantics.raw3184 line 174
  44. def OAI.MUB6.Certificate.PairSemantics.raw3184step0 line 176
  45. def OAI.MUB6.Certificate.PairSemantics.raw3184step1 line 178
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical3184 line 180
  47. def OAI.MUB6.Certificate.PairSemantics.raw3185 line 193
  48. def OAI.MUB6.Certificate.PairSemantics.raw3185step0 line 195
  49. def OAI.MUB6.Certificate.PairSemantics.raw3185step1 line 197
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical3185 line 199
  51. def OAI.MUB6.Certificate.PairSemantics.raw3186 line 212
  52. def OAI.MUB6.Certificate.PairSemantics.raw3186step0 line 214
  53. def OAI.MUB6.Certificate.PairSemantics.raw3186step1 line 216
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical3186 line 218
  55. def OAI.MUB6.Certificate.PairSemantics.raw3187 line 231
  56. def OAI.MUB6.Certificate.PairSemantics.raw3187step0 line 233
  57. def OAI.MUB6.Certificate.PairSemantics.raw3187step1 line 235
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical3187 line 237
  59. def OAI.MUB6.Certificate.PairSemantics.raw3188 line 250
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical3188 line 252
  61. def OAI.MUB6.Certificate.PairSemantics.raw3189 line 256
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical3189 line 258
  63. def OAI.MUB6.Certificate.PairSemantics.raw3190 line 262
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical3190 line 264
  65. def OAI.MUB6.Certificate.PairSemantics.raw3191 line 268
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical3191 line 270
  67. def OAI.MUB6.Certificate.PairSemantics.raw3192 line 274
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical3192 line 276
  69. def OAI.MUB6.Certificate.PairSemantics.raw3193 line 280
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical3193 line 282
  71. def OAI.MUB6.Certificate.PairSemantics.raw3194 line 286
  72. def OAI.MUB6.Certificate.PairSemantics.raw3194step0 line 288
  73. def OAI.MUB6.Certificate.PairSemantics.raw3194step1 line 290
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical3194 line 292
  75. def OAI.MUB6.Certificate.PairSemantics.raw3195 line 305
  76. def OAI.MUB6.Certificate.PairSemantics.raw3195step0 line 307
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical3195 line 309
  78. def OAI.MUB6.Certificate.PairSemantics.raw3196 line 318
  79. def OAI.MUB6.Certificate.PairSemantics.raw3196step0 line 320
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical3196 line 322
  81. def OAI.MUB6.Certificate.PairSemantics.raw3197 line 331
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical3197 line 333
  83. def OAI.MUB6.Certificate.PairSemantics.raw3198 line 337
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical3198 line 339
  85. def OAI.MUB6.Certificate.PairSemantics.raw3199 line 343
  86. def OAI.MUB6.Certificate.PairSemantics.raw3199step0 line 345
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical3199 line 347