OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical262.lean

GitHub source file

125 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8384 line 26
  2. def OAI.MUB6.Certificate.PairSemantics.raw8384step0 line 28
  3. theorem OAI.MUB6.Certificate.PairSemantics.canonical8384 line 30
  4. def OAI.MUB6.Certificate.PairSemantics.raw8385 line 39
  5. def OAI.MUB6.Certificate.PairSemantics.raw8385step0 line 41
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical8385 line 43
  7. def OAI.MUB6.Certificate.PairSemantics.raw8386 line 52
  8. def OAI.MUB6.Certificate.PairSemantics.raw8386step0 line 54
  9. def OAI.MUB6.Certificate.PairSemantics.raw8386step1 line 56
  10. def OAI.MUB6.Certificate.PairSemantics.raw8386step2 line 58
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical8386 line 60
  12. def OAI.MUB6.Certificate.PairSemantics.raw8387 line 78
  13. def OAI.MUB6.Certificate.PairSemantics.raw8387step0 line 80
  14. def OAI.MUB6.Certificate.PairSemantics.raw8387step1 line 82
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical8387 line 84
  16. def OAI.MUB6.Certificate.PairSemantics.raw8388 line 97
  17. def OAI.MUB6.Certificate.PairSemantics.raw8388step0 line 99
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical8388 line 101
  19. def OAI.MUB6.Certificate.PairSemantics.raw8389 line 110
  20. def OAI.MUB6.Certificate.PairSemantics.raw8389step0 line 112
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical8389 line 114
  22. def OAI.MUB6.Certificate.PairSemantics.raw8390 line 123
  23. def OAI.MUB6.Certificate.PairSemantics.raw8390step0 line 125
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical8390 line 127
  25. def OAI.MUB6.Certificate.PairSemantics.raw8391 line 136
  26. def OAI.MUB6.Certificate.PairSemantics.raw8391step0 line 138
  27. def OAI.MUB6.Certificate.PairSemantics.raw8391step1 line 140
  28. def OAI.MUB6.Certificate.PairSemantics.raw8391step2 line 142
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical8391 line 144
  30. def OAI.MUB6.Certificate.PairSemantics.raw8392 line 161
  31. def OAI.MUB6.Certificate.PairSemantics.raw8392step0 line 163
  32. def OAI.MUB6.Certificate.PairSemantics.raw8392step1 line 165
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical8392 line 167
  34. def OAI.MUB6.Certificate.PairSemantics.raw8393 line 180
  35. def OAI.MUB6.Certificate.PairSemantics.raw8393step0 line 182
  36. def OAI.MUB6.Certificate.PairSemantics.raw8393step1 line 184
  37. def OAI.MUB6.Certificate.PairSemantics.raw8393step2 line 186
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical8393 line 188
  39. def OAI.MUB6.Certificate.PairSemantics.raw8394 line 206
  40. def OAI.MUB6.Certificate.PairSemantics.raw8394step0 line 208
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical8394 line 210
  42. def OAI.MUB6.Certificate.PairSemantics.raw8395 line 219
  43. def OAI.MUB6.Certificate.PairSemantics.raw8395step0 line 221
  44. def OAI.MUB6.Certificate.PairSemantics.raw8395step1 line 223
  45. def OAI.MUB6.Certificate.PairSemantics.raw8395step2 line 225
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical8395 line 227
  47. def OAI.MUB6.Certificate.PairSemantics.raw8396 line 245
  48. def OAI.MUB6.Certificate.PairSemantics.raw8396step0 line 247
  49. def OAI.MUB6.Certificate.PairSemantics.raw8396step1 line 249
  50. def OAI.MUB6.Certificate.PairSemantics.raw8396step2 line 251
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical8396 line 253
  52. def OAI.MUB6.Certificate.PairSemantics.raw8397 line 271
  53. def OAI.MUB6.Certificate.PairSemantics.raw8397step0 line 273
  54. def OAI.MUB6.Certificate.PairSemantics.raw8397step1 line 275
  55. def OAI.MUB6.Certificate.PairSemantics.raw8397step2 line 277
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical8397 line 279
  57. def OAI.MUB6.Certificate.PairSemantics.raw8398 line 297
  58. def OAI.MUB6.Certificate.PairSemantics.raw8398step0 line 299
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical8398 line 301
  60. def OAI.MUB6.Certificate.PairSemantics.raw8399 line 310
  61. def OAI.MUB6.Certificate.PairSemantics.raw8399step0 line 312
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical8399 line 314
  63. def OAI.MUB6.Certificate.PairSemantics.raw8400 line 323
  64. def OAI.MUB6.Certificate.PairSemantics.raw8400step0 line 325
  65. def OAI.MUB6.Certificate.PairSemantics.raw8400step1 line 327
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical8400 line 329
  67. def OAI.MUB6.Certificate.PairSemantics.raw8401 line 342
  68. def OAI.MUB6.Certificate.PairSemantics.raw8401step0 line 344
  69. def OAI.MUB6.Certificate.PairSemantics.raw8401step1 line 346
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical8401 line 348
  71. def OAI.MUB6.Certificate.PairSemantics.raw8402 line 361
  72. def OAI.MUB6.Certificate.PairSemantics.raw8402step0 line 363
  73. def OAI.MUB6.Certificate.PairSemantics.raw8402step1 line 365
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical8402 line 367
  75. def OAI.MUB6.Certificate.PairSemantics.raw8403 line 380
  76. def OAI.MUB6.Certificate.PairSemantics.raw8403step0 line 382
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical8403 line 384
  78. def OAI.MUB6.Certificate.PairSemantics.raw8404 line 393
  79. def OAI.MUB6.Certificate.PairSemantics.raw8404step0 line 395
  80. def OAI.MUB6.Certificate.PairSemantics.raw8404step1 line 397
  81. def OAI.MUB6.Certificate.PairSemantics.raw8404step2 line 399
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical8404 line 401
  83. def OAI.MUB6.Certificate.PairSemantics.raw8405 line 419
  84. def OAI.MUB6.Certificate.PairSemantics.raw8405step0 line 421
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical8405 line 423
  86. def OAI.MUB6.Certificate.PairSemantics.raw8406 line 432
  87. def OAI.MUB6.Certificate.PairSemantics.raw8406step0 line 434
  88. def OAI.MUB6.Certificate.PairSemantics.raw8406step1 line 436
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical8406 line 438
  90. def OAI.MUB6.Certificate.PairSemantics.raw8407 line 451
  91. def OAI.MUB6.Certificate.PairSemantics.raw8407step0 line 453
  92. def OAI.MUB6.Certificate.PairSemantics.raw8407step1 line 455
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical8407 line 457
  94. def OAI.MUB6.Certificate.PairSemantics.raw8408 line 471
  95. def OAI.MUB6.Certificate.PairSemantics.raw8408step0 line 473
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical8408 line 475
  97. def OAI.MUB6.Certificate.PairSemantics.raw8409 line 484
  98. def OAI.MUB6.Certificate.PairSemantics.raw8409step0 line 486
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical8409 line 488
  100. def OAI.MUB6.Certificate.PairSemantics.raw8410 line 497
  101. def OAI.MUB6.Certificate.PairSemantics.raw8410step0 line 499
  102. def OAI.MUB6.Certificate.PairSemantics.raw8410step1 line 501
  103. def OAI.MUB6.Certificate.PairSemantics.raw8410step2 line 503
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical8410 line 505
  105. def OAI.MUB6.Certificate.PairSemantics.raw8411 line 523
  106. def OAI.MUB6.Certificate.PairSemantics.raw8411step0 line 525
  107. def OAI.MUB6.Certificate.PairSemantics.raw8411step1 line 527
  108. def OAI.MUB6.Certificate.PairSemantics.raw8411step2 line 529
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical8411 line 531
  110. def OAI.MUB6.Certificate.PairSemantics.raw8412 line 549
  111. def OAI.MUB6.Certificate.PairSemantics.raw8412step0 line 551
  112. def OAI.MUB6.Certificate.PairSemantics.raw8412step1 line 553
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical8412 line 555
  114. def OAI.MUB6.Certificate.PairSemantics.raw8413 line 568
  115. def OAI.MUB6.Certificate.PairSemantics.raw8413step0 line 570
  116. def OAI.MUB6.Certificate.PairSemantics.raw8413step1 line 572
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical8413 line 574
  118. def OAI.MUB6.Certificate.PairSemantics.raw8414 line 587
  119. def OAI.MUB6.Certificate.PairSemantics.raw8414step0 line 589
  120. def OAI.MUB6.Certificate.PairSemantics.raw8414step1 line 591
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical8414 line 593
  122. def OAI.MUB6.Certificate.PairSemantics.raw8415 line 607
  123. def OAI.MUB6.Certificate.PairSemantics.raw8415step0 line 609
  124. def OAI.MUB6.Certificate.PairSemantics.raw8415step1 line 611
  125. theorem OAI.MUB6.Certificate.PairSemantics.canonical8415 line 613