OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical6.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw192 line 11
  2. def OAI.MUB6.Certificate.PairSemantics.raw192step0 line 13
  3. def OAI.MUB6.Certificate.PairSemantics.raw192step1 line 15
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical192 line 17
  5. def OAI.MUB6.Certificate.PairSemantics.raw193 line 32
  6. def OAI.MUB6.Certificate.PairSemantics.raw193step0 line 34
  7. def OAI.MUB6.Certificate.PairSemantics.raw193step1 line 36
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical193 line 38
  9. def OAI.MUB6.Certificate.PairSemantics.raw194 line 53
  10. def OAI.MUB6.Certificate.PairSemantics.raw194step0 line 55
  11. def OAI.MUB6.Certificate.PairSemantics.raw194step1 line 57
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical194 line 59
  13. def OAI.MUB6.Certificate.PairSemantics.raw195 line 74
  14. def OAI.MUB6.Certificate.PairSemantics.raw195step0 line 76
  15. def OAI.MUB6.Certificate.PairSemantics.raw195step1 line 78
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical195 line 80
  17. def OAI.MUB6.Certificate.PairSemantics.raw196 line 95
  18. def OAI.MUB6.Certificate.PairSemantics.raw196step0 line 97
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical196 line 99
  20. def OAI.MUB6.Certificate.PairSemantics.raw197 line 109
  21. def OAI.MUB6.Certificate.PairSemantics.raw197step0 line 111
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical197 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw198 line 123
  24. def OAI.MUB6.Certificate.PairSemantics.raw198step0 line 125
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical198 line 127
  26. def OAI.MUB6.Certificate.PairSemantics.raw199 line 137
  27. def OAI.MUB6.Certificate.PairSemantics.raw199step0 line 139
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical199 line 141
  29. def OAI.MUB6.Certificate.PairSemantics.raw200 line 151
  30. def OAI.MUB6.Certificate.PairSemantics.raw200step0 line 153
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical200 line 155
  32. def OAI.MUB6.Certificate.PairSemantics.raw201 line 165
  33. def OAI.MUB6.Certificate.PairSemantics.raw201step0 line 167
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical201 line 169
  35. def OAI.MUB6.Certificate.PairSemantics.raw202 line 179
  36. def OAI.MUB6.Certificate.PairSemantics.raw202step0 line 181
  37. def OAI.MUB6.Certificate.PairSemantics.raw202step1 line 183
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical202 line 185
  39. def OAI.MUB6.Certificate.PairSemantics.raw203 line 199
  40. def OAI.MUB6.Certificate.PairSemantics.raw203step0 line 201
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical203 line 203
  42. def OAI.MUB6.Certificate.PairSemantics.raw204 line 213
  43. def OAI.MUB6.Certificate.PairSemantics.raw204step0 line 215
  44. def OAI.MUB6.Certificate.PairSemantics.raw204step1 line 217
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical204 line 219
  46. def OAI.MUB6.Certificate.PairSemantics.raw205 line 234
  47. def OAI.MUB6.Certificate.PairSemantics.raw205step0 line 236
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical205 line 238
  49. def OAI.MUB6.Certificate.PairSemantics.raw206 line 248
  50. def OAI.MUB6.Certificate.PairSemantics.raw206step0 line 250
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical206 line 252
  52. def OAI.MUB6.Certificate.PairSemantics.raw207 line 262
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical207 line 264
  54. def OAI.MUB6.Certificate.PairSemantics.raw208 line 268
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical208 line 270
  56. def OAI.MUB6.Certificate.PairSemantics.raw209 line 274
  57. def OAI.MUB6.Certificate.PairSemantics.raw209step0 line 276
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical209 line 278
  59. def OAI.MUB6.Certificate.PairSemantics.raw210 line 288
  60. def OAI.MUB6.Certificate.PairSemantics.raw210step0 line 290
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical210 line 292
  62. def OAI.MUB6.Certificate.PairSemantics.raw211 line 301
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical211 line 303
  64. def OAI.MUB6.Certificate.PairSemantics.raw212 line 307
  65. def OAI.MUB6.Certificate.PairSemantics.raw212step0 line 309
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical212 line 311
  67. def OAI.MUB6.Certificate.PairSemantics.raw213 line 321
  68. def OAI.MUB6.Certificate.PairSemantics.raw213step0 line 323
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical213 line 325
  70. def OAI.MUB6.Certificate.PairSemantics.raw214 line 334
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical214 line 336
  72. def OAI.MUB6.Certificate.PairSemantics.raw215 line 340
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical215 line 342
  74. def OAI.MUB6.Certificate.PairSemantics.raw216 line 346
  75. def OAI.MUB6.Certificate.PairSemantics.raw216step0 line 348
  76. def OAI.MUB6.Certificate.PairSemantics.raw216step1 line 350
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical216 line 352
  78. def OAI.MUB6.Certificate.PairSemantics.raw217 line 365
  79. def OAI.MUB6.Certificate.PairSemantics.raw217step0 line 367
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical217 line 369
  81. def OAI.MUB6.Certificate.PairSemantics.raw218 line 378
  82. def OAI.MUB6.Certificate.PairSemantics.raw218step0 line 380
  83. def OAI.MUB6.Certificate.PairSemantics.raw218step1 line 382
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical218 line 384
  85. def OAI.MUB6.Certificate.PairSemantics.raw219 line 397
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical219 line 399
  87. def OAI.MUB6.Certificate.PairSemantics.raw220 line 403
  88. def OAI.MUB6.Certificate.PairSemantics.raw220step0 line 405
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical220 line 407
  90. def OAI.MUB6.Certificate.PairSemantics.raw221 line 416
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical221 line 418
  92. def OAI.MUB6.Certificate.PairSemantics.raw222 line 422
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical222 line 424
  94. def OAI.MUB6.Certificate.PairSemantics.raw223 line 428
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical223 line 430