OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical68.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw2176 line 20
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical2176 line 22
  3. def OAI.MUB6.Certificate.PairSemantics.raw2177 line 26
  4. def OAI.MUB6.Certificate.PairSemantics.raw2177step0 line 28
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical2177 line 30
  6. def OAI.MUB6.Certificate.PairSemantics.raw2178 line 39
  7. def OAI.MUB6.Certificate.PairSemantics.raw2178step0 line 41
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical2178 line 43
  9. def OAI.MUB6.Certificate.PairSemantics.raw2179 line 52
  10. def OAI.MUB6.Certificate.PairSemantics.raw2179step0 line 54
  11. def OAI.MUB6.Certificate.PairSemantics.raw2179step1 line 56
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical2179 line 58
  13. def OAI.MUB6.Certificate.PairSemantics.raw2180 line 71
  14. def OAI.MUB6.Certificate.PairSemantics.raw2180step0 line 73
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical2180 line 75
  16. def OAI.MUB6.Certificate.PairSemantics.raw2181 line 84
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical2181 line 86
  18. def OAI.MUB6.Certificate.PairSemantics.raw2182 line 90
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical2182 line 92
  20. def OAI.MUB6.Certificate.PairSemantics.raw2183 line 96
  21. def OAI.MUB6.Certificate.PairSemantics.raw2183step0 line 98
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical2183 line 100
  23. def OAI.MUB6.Certificate.PairSemantics.raw2184 line 109
  24. def OAI.MUB6.Certificate.PairSemantics.raw2184step0 line 111
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical2184 line 113
  26. def OAI.MUB6.Certificate.PairSemantics.raw2185 line 122
  27. def OAI.MUB6.Certificate.PairSemantics.raw2185step0 line 124
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical2185 line 126
  29. def OAI.MUB6.Certificate.PairSemantics.raw2186 line 135
  30. def OAI.MUB6.Certificate.PairSemantics.raw2186step0 line 137
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical2186 line 139
  32. def OAI.MUB6.Certificate.PairSemantics.raw2187 line 148
  33. def OAI.MUB6.Certificate.PairSemantics.raw2187step0 line 150
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical2187 line 152
  35. def OAI.MUB6.Certificate.PairSemantics.raw2188 line 161
  36. def OAI.MUB6.Certificate.PairSemantics.raw2188step0 line 163
  37. def OAI.MUB6.Certificate.PairSemantics.raw2188step1 line 165
  38. def OAI.MUB6.Certificate.PairSemantics.raw2188step2 line 167
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical2188 line 169
  40. def OAI.MUB6.Certificate.PairSemantics.raw2189 line 186
  41. def OAI.MUB6.Certificate.PairSemantics.raw2189step0 line 188
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical2189 line 190
  43. def OAI.MUB6.Certificate.PairSemantics.raw2190 line 199
  44. def OAI.MUB6.Certificate.PairSemantics.raw2190step0 line 201
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical2190 line 203
  46. def OAI.MUB6.Certificate.PairSemantics.raw2191 line 212
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical2191 line 214
  48. def OAI.MUB6.Certificate.PairSemantics.raw2192 line 218
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical2192 line 220
  50. def OAI.MUB6.Certificate.PairSemantics.raw2193 line 224
  51. def OAI.MUB6.Certificate.PairSemantics.raw2193step0 line 226
  52. def OAI.MUB6.Certificate.PairSemantics.raw2193step1 line 228
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical2193 line 230
  54. def OAI.MUB6.Certificate.PairSemantics.raw2194 line 243
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical2194 line 245
  56. def OAI.MUB6.Certificate.PairSemantics.raw2195 line 249
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical2195 line 251
  58. def OAI.MUB6.Certificate.PairSemantics.raw2196 line 255
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical2196 line 257
  60. def OAI.MUB6.Certificate.PairSemantics.raw2197 line 261
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical2197 line 263
  62. def OAI.MUB6.Certificate.PairSemantics.raw2198 line 267
  63. def OAI.MUB6.Certificate.PairSemantics.raw2198step0 line 269
  64. def OAI.MUB6.Certificate.PairSemantics.raw2198step1 line 271
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical2198 line 273
  66. def OAI.MUB6.Certificate.PairSemantics.raw2199 line 286
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical2199 line 288
  68. def OAI.MUB6.Certificate.PairSemantics.raw2200 line 292
  69. def OAI.MUB6.Certificate.PairSemantics.raw2200step0 line 294
  70. def OAI.MUB6.Certificate.PairSemantics.raw2200step1 line 296
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical2200 line 298
  72. def OAI.MUB6.Certificate.PairSemantics.raw2201 line 311
  73. def OAI.MUB6.Certificate.PairSemantics.raw2201step0 line 313
  74. def OAI.MUB6.Certificate.PairSemantics.raw2201step1 line 315
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical2201 line 317
  76. def OAI.MUB6.Certificate.PairSemantics.raw2202 line 330
  77. def OAI.MUB6.Certificate.PairSemantics.raw2202step0 line 332
  78. def OAI.MUB6.Certificate.PairSemantics.raw2202step1 line 334
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical2202 line 336
  80. def OAI.MUB6.Certificate.PairSemantics.raw2203 line 349
  81. def OAI.MUB6.Certificate.PairSemantics.raw2203step0 line 351
  82. def OAI.MUB6.Certificate.PairSemantics.raw2203step1 line 353
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical2203 line 355
  84. def OAI.MUB6.Certificate.PairSemantics.raw2204 line 368
  85. def OAI.MUB6.Certificate.PairSemantics.raw2204step0 line 370
  86. def OAI.MUB6.Certificate.PairSemantics.raw2204step1 line 372
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical2204 line 374
  88. def OAI.MUB6.Certificate.PairSemantics.raw2205 line 387
  89. def OAI.MUB6.Certificate.PairSemantics.raw2205step0 line 389
  90. def OAI.MUB6.Certificate.PairSemantics.raw2205step1 line 391
  91. def OAI.MUB6.Certificate.PairSemantics.raw2205step2 line 393
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical2205 line 395
  93. def OAI.MUB6.Certificate.PairSemantics.raw2206 line 412
  94. def OAI.MUB6.Certificate.PairSemantics.raw2206step0 line 414
  95. def OAI.MUB6.Certificate.PairSemantics.raw2206step1 line 416
  96. def OAI.MUB6.Certificate.PairSemantics.raw2206step2 line 418
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical2206 line 420
  98. def OAI.MUB6.Certificate.PairSemantics.raw2207 line 437
  99. def OAI.MUB6.Certificate.PairSemantics.raw2207step0 line 439
  100. def OAI.MUB6.Certificate.PairSemantics.raw2207step1 line 441
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical2207 line 443