OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical194.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6208 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw6208step0 line 17
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical6208 line 19
  4. def OAI.MUB6.Certificate.PairSemantics.raw6209 line 28
  5. def OAI.MUB6.Certificate.PairSemantics.raw6209step0 line 30
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical6209 line 32
  7. def OAI.MUB6.Certificate.PairSemantics.raw6210 line 41
  8. def OAI.MUB6.Certificate.PairSemantics.raw6210step0 line 43
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical6210 line 45
  10. def OAI.MUB6.Certificate.PairSemantics.raw6211 line 54
  11. def OAI.MUB6.Certificate.PairSemantics.raw6211step0 line 56
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical6211 line 58
  13. def OAI.MUB6.Certificate.PairSemantics.raw6212 line 67
  14. def OAI.MUB6.Certificate.PairSemantics.raw6212step0 line 69
  15. def OAI.MUB6.Certificate.PairSemantics.raw6212step1 line 71
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical6212 line 73
  17. def OAI.MUB6.Certificate.PairSemantics.raw6213 line 86
  18. def OAI.MUB6.Certificate.PairSemantics.raw6213step0 line 88
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical6213 line 90
  20. def OAI.MUB6.Certificate.PairSemantics.raw6214 line 99
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical6214 line 101
  22. def OAI.MUB6.Certificate.PairSemantics.raw6215 line 105
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical6215 line 107
  24. def OAI.MUB6.Certificate.PairSemantics.raw6216 line 111
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical6216 line 113
  26. def OAI.MUB6.Certificate.PairSemantics.raw6217 line 117
  27. def OAI.MUB6.Certificate.PairSemantics.raw6217step0 line 119
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical6217 line 121
  29. def OAI.MUB6.Certificate.PairSemantics.raw6218 line 130
  30. def OAI.MUB6.Certificate.PairSemantics.raw6218step0 line 132
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical6218 line 134
  32. def OAI.MUB6.Certificate.PairSemantics.raw6219 line 143
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical6219 line 145
  34. def OAI.MUB6.Certificate.PairSemantics.raw6220 line 149
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical6220 line 151
  36. def OAI.MUB6.Certificate.PairSemantics.raw6221 line 155
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical6221 line 157
  38. def OAI.MUB6.Certificate.PairSemantics.raw6222 line 161
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical6222 line 163
  40. def OAI.MUB6.Certificate.PairSemantics.raw6223 line 167
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical6223 line 169
  42. def OAI.MUB6.Certificate.PairSemantics.raw6224 line 173
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical6224 line 175
  44. def OAI.MUB6.Certificate.PairSemantics.raw6225 line 179
  45. def OAI.MUB6.Certificate.PairSemantics.raw6225step0 line 181
  46. def OAI.MUB6.Certificate.PairSemantics.raw6225step1 line 183
  47. def OAI.MUB6.Certificate.PairSemantics.raw6225step2 line 185
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical6225 line 187
  49. def OAI.MUB6.Certificate.PairSemantics.raw6226 line 204
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical6226 line 206
  51. def OAI.MUB6.Certificate.PairSemantics.raw6227 line 210
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical6227 line 212
  53. def OAI.MUB6.Certificate.PairSemantics.raw6228 line 216
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical6228 line 218
  55. def OAI.MUB6.Certificate.PairSemantics.raw6229 line 222
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical6229 line 224
  57. def OAI.MUB6.Certificate.PairSemantics.raw6230 line 228
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical6230 line 230
  59. def OAI.MUB6.Certificate.PairSemantics.raw6231 line 234
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical6231 line 236
  61. def OAI.MUB6.Certificate.PairSemantics.raw6232 line 240
  62. def OAI.MUB6.Certificate.PairSemantics.raw6232step0 line 242
  63. def OAI.MUB6.Certificate.PairSemantics.raw6232step1 line 244
  64. def OAI.MUB6.Certificate.PairSemantics.raw6232step2 line 246
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical6232 line 248
  66. def OAI.MUB6.Certificate.PairSemantics.raw6233 line 265
  67. def OAI.MUB6.Certificate.PairSemantics.raw6233step0 line 267
  68. def OAI.MUB6.Certificate.PairSemantics.raw6233step1 line 269
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical6233 line 271
  70. def OAI.MUB6.Certificate.PairSemantics.raw6234 line 284
  71. def OAI.MUB6.Certificate.PairSemantics.raw6234step0 line 286
  72. def OAI.MUB6.Certificate.PairSemantics.raw6234step1 line 288
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical6234 line 290
  74. def OAI.MUB6.Certificate.PairSemantics.raw6235 line 303
  75. def OAI.MUB6.Certificate.PairSemantics.raw6235step0 line 305
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical6235 line 307
  77. def OAI.MUB6.Certificate.PairSemantics.raw6236 line 316
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical6236 line 318
  79. def OAI.MUB6.Certificate.PairSemantics.raw6237 line 322
  80. def OAI.MUB6.Certificate.PairSemantics.raw6237step0 line 324
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical6237 line 326
  82. def OAI.MUB6.Certificate.PairSemantics.raw6238 line 335
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical6238 line 337
  84. def OAI.MUB6.Certificate.PairSemantics.raw6239 line 341
  85. def OAI.MUB6.Certificate.PairSemantics.raw6239step0 line 343
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical6239 line 345