OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical251.lean

GitHub source file

124 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw8032 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw8032step0 line 23
  3. def OAI.MUB6.Certificate.PairSemantics.raw8032step1 line 25
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical8032 line 27
  5. def OAI.MUB6.Certificate.PairSemantics.raw8033 line 40
  6. def OAI.MUB6.Certificate.PairSemantics.raw8033step0 line 42
  7. def OAI.MUB6.Certificate.PairSemantics.raw8033step1 line 44
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical8033 line 46
  9. def OAI.MUB6.Certificate.PairSemantics.raw8034 line 59
  10. def OAI.MUB6.Certificate.PairSemantics.raw8034step0 line 61
  11. def OAI.MUB6.Certificate.PairSemantics.raw8034step1 line 63
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical8034 line 65
  13. def OAI.MUB6.Certificate.PairSemantics.raw8035 line 78
  14. def OAI.MUB6.Certificate.PairSemantics.raw8035step0 line 80
  15. def OAI.MUB6.Certificate.PairSemantics.raw8035step1 line 82
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical8035 line 84
  17. def OAI.MUB6.Certificate.PairSemantics.raw8036 line 97
  18. def OAI.MUB6.Certificate.PairSemantics.raw8036step0 line 99
  19. def OAI.MUB6.Certificate.PairSemantics.raw8036step1 line 101
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical8036 line 103
  21. def OAI.MUB6.Certificate.PairSemantics.raw8037 line 116
  22. def OAI.MUB6.Certificate.PairSemantics.raw8037step0 line 118
  23. def OAI.MUB6.Certificate.PairSemantics.raw8037step1 line 120
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical8037 line 122
  25. def OAI.MUB6.Certificate.PairSemantics.raw8038 line 135
  26. def OAI.MUB6.Certificate.PairSemantics.raw8038step0 line 137
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical8038 line 139
  28. def OAI.MUB6.Certificate.PairSemantics.raw8039 line 148
  29. def OAI.MUB6.Certificate.PairSemantics.raw8039step0 line 150
  30. def OAI.MUB6.Certificate.PairSemantics.raw8039step1 line 152
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical8039 line 154
  32. def OAI.MUB6.Certificate.PairSemantics.raw8040 line 169
  33. def OAI.MUB6.Certificate.PairSemantics.raw8040step0 line 171
  34. def OAI.MUB6.Certificate.PairSemantics.raw8040step1 line 173
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical8040 line 175
  36. def OAI.MUB6.Certificate.PairSemantics.raw8041 line 188
  37. def OAI.MUB6.Certificate.PairSemantics.raw8041step0 line 190
  38. def OAI.MUB6.Certificate.PairSemantics.raw8041step1 line 192
  39. def OAI.MUB6.Certificate.PairSemantics.raw8041step2 line 194
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical8041 line 196
  41. def OAI.MUB6.Certificate.PairSemantics.raw8042 line 215
  42. def OAI.MUB6.Certificate.PairSemantics.raw8042step0 line 217
  43. def OAI.MUB6.Certificate.PairSemantics.raw8042step1 line 219
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical8042 line 221
  45. def OAI.MUB6.Certificate.PairSemantics.raw8043 line 235
  46. def OAI.MUB6.Certificate.PairSemantics.raw8043step0 line 237
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical8043 line 239
  48. def OAI.MUB6.Certificate.PairSemantics.raw8044 line 248
  49. def OAI.MUB6.Certificate.PairSemantics.raw8044step0 line 250
  50. def OAI.MUB6.Certificate.PairSemantics.raw8044step1 line 252
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical8044 line 254
  52. def OAI.MUB6.Certificate.PairSemantics.raw8045 line 267
  53. def OAI.MUB6.Certificate.PairSemantics.raw8045step0 line 269
  54. def OAI.MUB6.Certificate.PairSemantics.raw8045step1 line 271
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical8045 line 273
  56. def OAI.MUB6.Certificate.PairSemantics.raw8046 line 288
  57. def OAI.MUB6.Certificate.PairSemantics.raw8046step0 line 290
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical8046 line 292
  59. def OAI.MUB6.Certificate.PairSemantics.raw8047 line 302
  60. def OAI.MUB6.Certificate.PairSemantics.raw8047step0 line 304
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical8047 line 306
  62. def OAI.MUB6.Certificate.PairSemantics.raw8048 line 316
  63. def OAI.MUB6.Certificate.PairSemantics.raw8048step0 line 318
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical8048 line 320
  65. def OAI.MUB6.Certificate.PairSemantics.raw8049 line 330
  66. def OAI.MUB6.Certificate.PairSemantics.raw8049step0 line 332
  67. def OAI.MUB6.Certificate.PairSemantics.raw8049step1 line 334
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical8049 line 336
  69. def OAI.MUB6.Certificate.PairSemantics.raw8050 line 349
  70. def OAI.MUB6.Certificate.PairSemantics.raw8050step0 line 351
  71. def OAI.MUB6.Certificate.PairSemantics.raw8050step1 line 353
  72. def OAI.MUB6.Certificate.PairSemantics.raw8050step2 line 355
  73. def OAI.MUB6.Certificate.PairSemantics.raw8050step3 line 357
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical8050 line 359
  75. def OAI.MUB6.Certificate.PairSemantics.raw8051 line 382
  76. def OAI.MUB6.Certificate.PairSemantics.raw8051step0 line 384
  77. def OAI.MUB6.Certificate.PairSemantics.raw8051step1 line 386
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical8051 line 388
  79. def OAI.MUB6.Certificate.PairSemantics.raw8052 line 401
  80. def OAI.MUB6.Certificate.PairSemantics.raw8052step0 line 403
  81. def OAI.MUB6.Certificate.PairSemantics.raw8052step1 line 405
  82. def OAI.MUB6.Certificate.PairSemantics.raw8052step2 line 407
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical8052 line 409
  84. def OAI.MUB6.Certificate.PairSemantics.raw8053 line 428
  85. def OAI.MUB6.Certificate.PairSemantics.raw8053step0 line 430
  86. def OAI.MUB6.Certificate.PairSemantics.raw8053step1 line 432
  87. def OAI.MUB6.Certificate.PairSemantics.raw8053step2 line 434
  88. def OAI.MUB6.Certificate.PairSemantics.raw8053step3 line 436
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical8053 line 438
  90. def OAI.MUB6.Certificate.PairSemantics.raw8054 line 460
  91. def OAI.MUB6.Certificate.PairSemantics.raw8054step0 line 462
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical8054 line 464
  93. def OAI.MUB6.Certificate.PairSemantics.raw8055 line 473
  94. def OAI.MUB6.Certificate.PairSemantics.raw8055step0 line 475
  95. def OAI.MUB6.Certificate.PairSemantics.raw8055step1 line 477
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical8055 line 479
  97. def OAI.MUB6.Certificate.PairSemantics.raw8056 line 492
  98. def OAI.MUB6.Certificate.PairSemantics.raw8056step0 line 494
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical8056 line 496
  100. def OAI.MUB6.Certificate.PairSemantics.raw8057 line 505
  101. def OAI.MUB6.Certificate.PairSemantics.raw8057step0 line 507
  102. def OAI.MUB6.Certificate.PairSemantics.raw8057step1 line 509
  103. def OAI.MUB6.Certificate.PairSemantics.raw8057step2 line 511
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical8057 line 513
  105. def OAI.MUB6.Certificate.PairSemantics.raw8058 line 530
  106. def OAI.MUB6.Certificate.PairSemantics.raw8058step0 line 532
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical8058 line 534
  108. def OAI.MUB6.Certificate.PairSemantics.raw8059 line 543
  109. def OAI.MUB6.Certificate.PairSemantics.raw8059step0 line 545
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical8059 line 547
  111. def OAI.MUB6.Certificate.PairSemantics.raw8060 line 556
  112. def OAI.MUB6.Certificate.PairSemantics.raw8060step0 line 558
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical8060 line 560
  114. def OAI.MUB6.Certificate.PairSemantics.raw8061 line 569
  115. def OAI.MUB6.Certificate.PairSemantics.raw8061step0 line 571
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical8061 line 573
  117. def OAI.MUB6.Certificate.PairSemantics.raw8062 line 582
  118. def OAI.MUB6.Certificate.PairSemantics.raw8062step0 line 584
  119. def OAI.MUB6.Certificate.PairSemantics.raw8062step1 line 586
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical8062 line 588
  121. def OAI.MUB6.Certificate.PairSemantics.raw8063 line 601
  122. def OAI.MUB6.Certificate.PairSemantics.raw8063step0 line 603
  123. def OAI.MUB6.Certificate.PairSemantics.raw8063step1 line 605
  124. theorem OAI.MUB6.Certificate.PairSemantics.canonical8063 line 607