OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical100.lean

GitHub source file

111 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw3200 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw3200step0 line 20
  3. def OAI.MUB6.Certificate.PairSemantics.raw3200step1 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw3200step2 line 24
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical3200 line 26
  6. def OAI.MUB6.Certificate.PairSemantics.raw3201 line 43
  7. def OAI.MUB6.Certificate.PairSemantics.raw3201step0 line 45
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical3201 line 47
  9. def OAI.MUB6.Certificate.PairSemantics.raw3202 line 56
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical3202 line 58
  11. def OAI.MUB6.Certificate.PairSemantics.raw3203 line 62
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical3203 line 64
  13. def OAI.MUB6.Certificate.PairSemantics.raw3204 line 68
  14. def OAI.MUB6.Certificate.PairSemantics.raw3204step0 line 70
  15. def OAI.MUB6.Certificate.PairSemantics.raw3204step1 line 72
  16. def OAI.MUB6.Certificate.PairSemantics.raw3204step2 line 74
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical3204 line 76
  18. def OAI.MUB6.Certificate.PairSemantics.raw3205 line 93
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical3205 line 95
  20. def OAI.MUB6.Certificate.PairSemantics.raw3206 line 99
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical3206 line 101
  22. def OAI.MUB6.Certificate.PairSemantics.raw3207 line 105
  23. def OAI.MUB6.Certificate.PairSemantics.raw3207step0 line 107
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical3207 line 109
  25. def OAI.MUB6.Certificate.PairSemantics.raw3208 line 118
  26. def OAI.MUB6.Certificate.PairSemantics.raw3208step0 line 120
  27. def OAI.MUB6.Certificate.PairSemantics.raw3208step1 line 122
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical3208 line 124
  29. def OAI.MUB6.Certificate.PairSemantics.raw3209 line 137
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical3209 line 139
  31. def OAI.MUB6.Certificate.PairSemantics.raw3210 line 143
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical3210 line 145
  33. def OAI.MUB6.Certificate.PairSemantics.raw3211 line 149
  34. def OAI.MUB6.Certificate.PairSemantics.raw3211step0 line 151
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical3211 line 153
  36. def OAI.MUB6.Certificate.PairSemantics.raw3212 line 162
  37. def OAI.MUB6.Certificate.PairSemantics.raw3212step0 line 164
  38. def OAI.MUB6.Certificate.PairSemantics.raw3212step1 line 166
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical3212 line 168
  40. def OAI.MUB6.Certificate.PairSemantics.raw3213 line 181
  41. def OAI.MUB6.Certificate.PairSemantics.raw3213step0 line 183
  42. def OAI.MUB6.Certificate.PairSemantics.raw3213step1 line 185
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical3213 line 187
  44. def OAI.MUB6.Certificate.PairSemantics.raw3214 line 200
  45. def OAI.MUB6.Certificate.PairSemantics.raw3214step0 line 202
  46. def OAI.MUB6.Certificate.PairSemantics.raw3214step1 line 204
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical3214 line 206
  48. def OAI.MUB6.Certificate.PairSemantics.raw3215 line 219
  49. def OAI.MUB6.Certificate.PairSemantics.raw3215step0 line 221
  50. def OAI.MUB6.Certificate.PairSemantics.raw3215step1 line 223
  51. def OAI.MUB6.Certificate.PairSemantics.raw3215step2 line 225
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical3215 line 227
  53. def OAI.MUB6.Certificate.PairSemantics.raw3216 line 244
  54. def OAI.MUB6.Certificate.PairSemantics.raw3216step0 line 246
  55. def OAI.MUB6.Certificate.PairSemantics.raw3216step1 line 248
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical3216 line 250
  57. def OAI.MUB6.Certificate.PairSemantics.raw3217 line 263
  58. def OAI.MUB6.Certificate.PairSemantics.raw3217step0 line 265
  59. def OAI.MUB6.Certificate.PairSemantics.raw3217step1 line 267
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical3217 line 269
  61. def OAI.MUB6.Certificate.PairSemantics.raw3218 line 282
  62. def OAI.MUB6.Certificate.PairSemantics.raw3218step0 line 284
  63. def OAI.MUB6.Certificate.PairSemantics.raw3218step1 line 286
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical3218 line 288
  65. def OAI.MUB6.Certificate.PairSemantics.raw3219 line 301
  66. def OAI.MUB6.Certificate.PairSemantics.raw3219step0 line 303
  67. def OAI.MUB6.Certificate.PairSemantics.raw3219step1 line 305
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical3219 line 307
  69. def OAI.MUB6.Certificate.PairSemantics.raw3220 line 320
  70. def OAI.MUB6.Certificate.PairSemantics.raw3220step0 line 322
  71. def OAI.MUB6.Certificate.PairSemantics.raw3220step1 line 324
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical3220 line 326
  73. def OAI.MUB6.Certificate.PairSemantics.raw3221 line 339
  74. def OAI.MUB6.Certificate.PairSemantics.raw3221step0 line 341
  75. def OAI.MUB6.Certificate.PairSemantics.raw3221step1 line 343
  76. theorem OAI.MUB6.Certificate.PairSemantics.canonical3221 line 345
  77. def OAI.MUB6.Certificate.PairSemantics.raw3222 line 358
  78. def OAI.MUB6.Certificate.PairSemantics.raw3222step0 line 360
  79. def OAI.MUB6.Certificate.PairSemantics.raw3222step1 line 362
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical3222 line 364
  81. def OAI.MUB6.Certificate.PairSemantics.raw3223 line 377
  82. def OAI.MUB6.Certificate.PairSemantics.raw3223step0 line 379
  83. def OAI.MUB6.Certificate.PairSemantics.raw3223step1 line 381
  84. theorem OAI.MUB6.Certificate.PairSemantics.canonical3223 line 383
  85. def OAI.MUB6.Certificate.PairSemantics.raw3224 line 396
  86. def OAI.MUB6.Certificate.PairSemantics.raw3224step0 line 398
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical3224 line 400
  88. def OAI.MUB6.Certificate.PairSemantics.raw3225 line 409
  89. def OAI.MUB6.Certificate.PairSemantics.raw3225step0 line 411
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical3225 line 413
  91. def OAI.MUB6.Certificate.PairSemantics.raw3226 line 422
  92. def OAI.MUB6.Certificate.PairSemantics.raw3226step0 line 424
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical3226 line 426
  94. def OAI.MUB6.Certificate.PairSemantics.raw3227 line 435
  95. def OAI.MUB6.Certificate.PairSemantics.raw3227step0 line 437
  96. def OAI.MUB6.Certificate.PairSemantics.raw3227step1 line 439
  97. def OAI.MUB6.Certificate.PairSemantics.raw3227step2 line 441
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical3227 line 443
  99. def OAI.MUB6.Certificate.PairSemantics.raw3228 line 460
  100. def OAI.MUB6.Certificate.PairSemantics.raw3228step0 line 462
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical3228 line 464
  102. def OAI.MUB6.Certificate.PairSemantics.raw3229 line 473
  103. def OAI.MUB6.Certificate.PairSemantics.raw3229step0 line 475
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical3229 line 477
  105. def OAI.MUB6.Certificate.PairSemantics.raw3230 line 486
  106. def OAI.MUB6.Certificate.PairSemantics.raw3230step0 line 488
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical3230 line 490
  108. def OAI.MUB6.Certificate.PairSemantics.raw3231 line 499
  109. def OAI.MUB6.Certificate.PairSemantics.raw3231step0 line 501
  110. def OAI.MUB6.Certificate.PairSemantics.raw3231step1 line 503
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical3231 line 505