OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical286.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9152 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw9152step0 line 21
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical9152 line 23
  4. def OAI.MUB6.Certificate.PairSemantics.raw9153 line 32
  5. def OAI.MUB6.Certificate.PairSemantics.raw9153step0 line 34
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical9153 line 36
  7. def OAI.MUB6.Certificate.PairSemantics.raw9154 line 45
  8. def OAI.MUB6.Certificate.PairSemantics.raw9154step0 line 47
  9. def OAI.MUB6.Certificate.PairSemantics.raw9154step1 line 49
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical9154 line 51
  11. def OAI.MUB6.Certificate.PairSemantics.raw9155 line 65
  12. def OAI.MUB6.Certificate.PairSemantics.raw9155step0 line 67
  13. def OAI.MUB6.Certificate.PairSemantics.raw9155step1 line 69
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical9155 line 71
  15. def OAI.MUB6.Certificate.PairSemantics.raw9156 line 84
  16. def OAI.MUB6.Certificate.PairSemantics.raw9156step0 line 86
  17. def OAI.MUB6.Certificate.PairSemantics.raw9156step1 line 88
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical9156 line 90
  19. def OAI.MUB6.Certificate.PairSemantics.raw9157 line 103
  20. def OAI.MUB6.Certificate.PairSemantics.raw9157step0 line 105
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical9157 line 107
  22. def OAI.MUB6.Certificate.PairSemantics.raw9158 line 116
  23. def OAI.MUB6.Certificate.PairSemantics.raw9158step0 line 118
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical9158 line 120
  25. def OAI.MUB6.Certificate.PairSemantics.raw9159 line 129
  26. def OAI.MUB6.Certificate.PairSemantics.raw9159step0 line 131
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical9159 line 133
  28. def OAI.MUB6.Certificate.PairSemantics.raw9160 line 142
  29. def OAI.MUB6.Certificate.PairSemantics.raw9160step0 line 144
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical9160 line 146
  31. def OAI.MUB6.Certificate.PairSemantics.raw9161 line 155
  32. def OAI.MUB6.Certificate.PairSemantics.raw9161step0 line 157
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical9161 line 159
  34. def OAI.MUB6.Certificate.PairSemantics.raw9162 line 168
  35. def OAI.MUB6.Certificate.PairSemantics.raw9162step0 line 170
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical9162 line 172
  37. def OAI.MUB6.Certificate.PairSemantics.raw9163 line 181
  38. def OAI.MUB6.Certificate.PairSemantics.raw9163step0 line 183
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical9163 line 185
  40. def OAI.MUB6.Certificate.PairSemantics.raw9164 line 194
  41. def OAI.MUB6.Certificate.PairSemantics.raw9164step0 line 196
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical9164 line 198
  43. def OAI.MUB6.Certificate.PairSemantics.raw9165 line 207
  44. def OAI.MUB6.Certificate.PairSemantics.raw9165step0 line 209
  45. def OAI.MUB6.Certificate.PairSemantics.raw9165step1 line 211
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical9165 line 213
  47. def OAI.MUB6.Certificate.PairSemantics.raw9166 line 226
  48. def OAI.MUB6.Certificate.PairSemantics.raw9166step0 line 228
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical9166 line 230
  50. def OAI.MUB6.Certificate.PairSemantics.raw9167 line 239
  51. def OAI.MUB6.Certificate.PairSemantics.raw9167step0 line 241
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical9167 line 243
  53. def OAI.MUB6.Certificate.PairSemantics.raw9168 line 252
  54. def OAI.MUB6.Certificate.PairSemantics.raw9168step0 line 254
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical9168 line 256
  56. def OAI.MUB6.Certificate.PairSemantics.raw9169 line 265
  57. def OAI.MUB6.Certificate.PairSemantics.raw9169step0 line 267
  58. def OAI.MUB6.Certificate.PairSemantics.raw9169step1 line 269
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical9169 line 271
  60. def OAI.MUB6.Certificate.PairSemantics.raw9170 line 284
  61. def OAI.MUB6.Certificate.PairSemantics.raw9170step0 line 286
  62. def OAI.MUB6.Certificate.PairSemantics.raw9170step1 line 288
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical9170 line 290
  64. def OAI.MUB6.Certificate.PairSemantics.raw9171 line 303
  65. def OAI.MUB6.Certificate.PairSemantics.raw9171step0 line 305
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical9171 line 307
  67. def OAI.MUB6.Certificate.PairSemantics.raw9172 line 316
  68. def OAI.MUB6.Certificate.PairSemantics.raw9172step0 line 318
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical9172 line 320
  70. def OAI.MUB6.Certificate.PairSemantics.raw9173 line 329
  71. def OAI.MUB6.Certificate.PairSemantics.raw9173step0 line 331
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical9173 line 333
  73. def OAI.MUB6.Certificate.PairSemantics.raw9174 line 342
  74. def OAI.MUB6.Certificate.PairSemantics.raw9174step0 line 344
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical9174 line 346
  76. def OAI.MUB6.Certificate.PairSemantics.raw9175 line 355
  77. def OAI.MUB6.Certificate.PairSemantics.raw9175step0 line 357
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical9175 line 359
  79. def OAI.MUB6.Certificate.PairSemantics.raw9176 line 368
  80. def OAI.MUB6.Certificate.PairSemantics.raw9176step0 line 370
  81. def OAI.MUB6.Certificate.PairSemantics.raw9176step1 line 372
  82. def OAI.MUB6.Certificate.PairSemantics.raw9176step2 line 374
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical9176 line 376
  84. def OAI.MUB6.Certificate.PairSemantics.raw9177 line 394
  85. def OAI.MUB6.Certificate.PairSemantics.raw9177step0 line 396
  86. def OAI.MUB6.Certificate.PairSemantics.raw9177step1 line 398
  87. def OAI.MUB6.Certificate.PairSemantics.raw9177step2 line 400
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical9177 line 402
  89. def OAI.MUB6.Certificate.PairSemantics.raw9178 line 420
  90. def OAI.MUB6.Certificate.PairSemantics.raw9178step0 line 422
  91. def OAI.MUB6.Certificate.PairSemantics.raw9178step1 line 424
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical9178 line 426
  93. def OAI.MUB6.Certificate.PairSemantics.raw9179 line 439
  94. def OAI.MUB6.Certificate.PairSemantics.raw9179step0 line 441
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical9179 line 443
  96. def OAI.MUB6.Certificate.PairSemantics.raw9180 line 452
  97. def OAI.MUB6.Certificate.PairSemantics.raw9180step0 line 454
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical9180 line 456
  99. def OAI.MUB6.Certificate.PairSemantics.raw9181 line 465
  100. def OAI.MUB6.Certificate.PairSemantics.raw9181step0 line 467
  101. def OAI.MUB6.Certificate.PairSemantics.raw9181step1 line 469
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical9181 line 471
  103. def OAI.MUB6.Certificate.PairSemantics.raw9182 line 484
  104. def OAI.MUB6.Certificate.PairSemantics.raw9182step0 line 486
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical9182 line 488
  106. def OAI.MUB6.Certificate.PairSemantics.raw9183 line 497
  107. def OAI.MUB6.Certificate.PairSemantics.raw9183step0 line 499
  108. def OAI.MUB6.Certificate.PairSemantics.raw9183step1 line 501
  109. def OAI.MUB6.Certificate.PairSemantics.raw9183step2 line 503
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical9183 line 505