OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical69.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2208 line 15
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical2208 line 17
  3. def OAI.MUB6.Certificate.PairSemantics.raw2209 line 21
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical2209 line 23
  5. def OAI.MUB6.Certificate.PairSemantics.raw2210 line 27
  6. def OAI.MUB6.Certificate.PairSemantics.raw2210step0 line 29
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical2210 line 31
  8. def OAI.MUB6.Certificate.PairSemantics.raw2211 line 40
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical2211 line 42
  10. def OAI.MUB6.Certificate.PairSemantics.raw2212 line 46
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical2212 line 48
  12. def OAI.MUB6.Certificate.PairSemantics.raw2213 line 52
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical2213 line 54
  14. def OAI.MUB6.Certificate.PairSemantics.raw2214 line 58
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical2214 line 60
  16. def OAI.MUB6.Certificate.PairSemantics.raw2215 line 64
  17. def OAI.MUB6.Certificate.PairSemantics.raw2215step0 line 66
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical2215 line 68
  19. def OAI.MUB6.Certificate.PairSemantics.raw2216 line 77
  20. def OAI.MUB6.Certificate.PairSemantics.raw2216step0 line 79
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical2216 line 81
  22. def OAI.MUB6.Certificate.PairSemantics.raw2217 line 90
  23. def OAI.MUB6.Certificate.PairSemantics.raw2217step0 line 92
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical2217 line 94
  25. def OAI.MUB6.Certificate.PairSemantics.raw2218 line 103
  26. def OAI.MUB6.Certificate.PairSemantics.raw2218step0 line 105
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical2218 line 107
  28. def OAI.MUB6.Certificate.PairSemantics.raw2219 line 116
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical2219 line 118
  30. def OAI.MUB6.Certificate.PairSemantics.raw2220 line 122
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical2220 line 124
  32. def OAI.MUB6.Certificate.PairSemantics.raw2221 line 128
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical2221 line 130
  34. def OAI.MUB6.Certificate.PairSemantics.raw2222 line 134
  35. def OAI.MUB6.Certificate.PairSemantics.raw2222step0 line 136
  36. def OAI.MUB6.Certificate.PairSemantics.raw2222step1 line 138
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical2222 line 140
  38. def OAI.MUB6.Certificate.PairSemantics.raw2223 line 153
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical2223 line 155
  40. def OAI.MUB6.Certificate.PairSemantics.raw2224 line 159
  41. def OAI.MUB6.Certificate.PairSemantics.raw2224step0 line 161
  42. def OAI.MUB6.Certificate.PairSemantics.raw2224step1 line 163
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical2224 line 165
  44. def OAI.MUB6.Certificate.PairSemantics.raw2225 line 178
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical2225 line 180
  46. def OAI.MUB6.Certificate.PairSemantics.raw2226 line 184
  47. def OAI.MUB6.Certificate.PairSemantics.raw2226step0 line 186
  48. def OAI.MUB6.Certificate.PairSemantics.raw2226step1 line 188
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical2226 line 190
  50. def OAI.MUB6.Certificate.PairSemantics.raw2227 line 203
  51. def OAI.MUB6.Certificate.PairSemantics.raw2227step0 line 205
  52. def OAI.MUB6.Certificate.PairSemantics.raw2227step1 line 207
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical2227 line 209
  54. def OAI.MUB6.Certificate.PairSemantics.raw2228 line 222
  55. def OAI.MUB6.Certificate.PairSemantics.raw2228step0 line 224
  56. def OAI.MUB6.Certificate.PairSemantics.raw2228step1 line 226
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical2228 line 228
  58. def OAI.MUB6.Certificate.PairSemantics.raw2229 line 241
  59. def OAI.MUB6.Certificate.PairSemantics.raw2229step0 line 243
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical2229 line 245
  61. def OAI.MUB6.Certificate.PairSemantics.raw2230 line 254
  62. def OAI.MUB6.Certificate.PairSemantics.raw2230step0 line 256
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical2230 line 258
  64. def OAI.MUB6.Certificate.PairSemantics.raw2231 line 267
  65. def OAI.MUB6.Certificate.PairSemantics.raw2231step0 line 269
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical2231 line 271
  67. def OAI.MUB6.Certificate.PairSemantics.raw2232 line 280
  68. def OAI.MUB6.Certificate.PairSemantics.raw2232step0 line 282
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical2232 line 284
  70. def OAI.MUB6.Certificate.PairSemantics.raw2233 line 293
  71. def OAI.MUB6.Certificate.PairSemantics.raw2233step0 line 295
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical2233 line 297
  73. def OAI.MUB6.Certificate.PairSemantics.raw2234 line 306
  74. def OAI.MUB6.Certificate.PairSemantics.raw2234step0 line 308
  75. def OAI.MUB6.Certificate.PairSemantics.raw2234step1 line 310
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical2234 line 312
  77. def OAI.MUB6.Certificate.PairSemantics.raw2235 line 325
  78. def OAI.MUB6.Certificate.PairSemantics.raw2235step0 line 327
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical2235 line 329
  80. def OAI.MUB6.Certificate.PairSemantics.raw2236 line 338
  81. def OAI.MUB6.Certificate.PairSemantics.raw2236step0 line 340
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical2236 line 342
  83. def OAI.MUB6.Certificate.PairSemantics.raw2237 line 351
  84. def OAI.MUB6.Certificate.PairSemantics.raw2237step0 line 353
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical2237 line 355
  86. def OAI.MUB6.Certificate.PairSemantics.raw2238 line 364
  87. def OAI.MUB6.Certificate.PairSemantics.raw2238step0 line 366
  88. def OAI.MUB6.Certificate.PairSemantics.raw2238step1 line 368
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical2238 line 370
  90. def OAI.MUB6.Certificate.PairSemantics.raw2239 line 383
  91. def OAI.MUB6.Certificate.PairSemantics.raw2239step0 line 385
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical2239 line 387