OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical282.lean

GitHub source file

163 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9024 line 9
  2. def OAI.MUB6.Certificate.PairSemantics.raw9024step0 line 11
  3. def OAI.MUB6.Certificate.PairSemantics.raw9024step1 line 13
  4. def OAI.MUB6.Certificate.PairSemantics.raw9024step2 line 15
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical9024 line 17
  6. def OAI.MUB6.Certificate.PairSemantics.raw9025 line 36
  7. def OAI.MUB6.Certificate.PairSemantics.raw9025step0 line 38
  8. def OAI.MUB6.Certificate.PairSemantics.raw9025step1 line 40
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical9025 line 42
  10. def OAI.MUB6.Certificate.PairSemantics.raw9026 line 56
  11. def OAI.MUB6.Certificate.PairSemantics.raw9026step0 line 58
  12. def OAI.MUB6.Certificate.PairSemantics.raw9026step1 line 60
  13. def OAI.MUB6.Certificate.PairSemantics.raw9026step2 line 62
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical9026 line 64
  15. def OAI.MUB6.Certificate.PairSemantics.raw9027 line 83
  16. def OAI.MUB6.Certificate.PairSemantics.raw9027step0 line 85
  17. def OAI.MUB6.Certificate.PairSemantics.raw9027step1 line 87
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical9027 line 89
  19. def OAI.MUB6.Certificate.PairSemantics.raw9028 line 104
  20. def OAI.MUB6.Certificate.PairSemantics.raw9028step0 line 106
  21. def OAI.MUB6.Certificate.PairSemantics.raw9028step1 line 108
  22. def OAI.MUB6.Certificate.PairSemantics.raw9028step2 line 110
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical9028 line 112
  24. def OAI.MUB6.Certificate.PairSemantics.raw9029 line 132
  25. def OAI.MUB6.Certificate.PairSemantics.raw9029step0 line 134
  26. def OAI.MUB6.Certificate.PairSemantics.raw9029step1 line 136
  27. def OAI.MUB6.Certificate.PairSemantics.raw9029step2 line 138
  28. def OAI.MUB6.Certificate.PairSemantics.raw9029step3 line 140
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical9029 line 142
  30. def OAI.MUB6.Certificate.PairSemantics.raw9030 line 167
  31. def OAI.MUB6.Certificate.PairSemantics.raw9030step0 line 169
  32. def OAI.MUB6.Certificate.PairSemantics.raw9030step1 line 171
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical9030 line 173
  34. def OAI.MUB6.Certificate.PairSemantics.raw9031 line 187
  35. def OAI.MUB6.Certificate.PairSemantics.raw9031step0 line 189
  36. def OAI.MUB6.Certificate.PairSemantics.raw9031step1 line 191
  37. def OAI.MUB6.Certificate.PairSemantics.raw9031step2 line 193
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical9031 line 195
  39. def OAI.MUB6.Certificate.PairSemantics.raw9032 line 214
  40. def OAI.MUB6.Certificate.PairSemantics.raw9032step0 line 216
  41. def OAI.MUB6.Certificate.PairSemantics.raw9032step1 line 218
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical9032 line 220
  43. def OAI.MUB6.Certificate.PairSemantics.raw9033 line 234
  44. def OAI.MUB6.Certificate.PairSemantics.raw9033step0 line 236
  45. def OAI.MUB6.Certificate.PairSemantics.raw9033step1 line 238
  46. def OAI.MUB6.Certificate.PairSemantics.raw9033step2 line 240
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical9033 line 242
  48. def OAI.MUB6.Certificate.PairSemantics.raw9034 line 261
  49. def OAI.MUB6.Certificate.PairSemantics.raw9034step0 line 263
  50. def OAI.MUB6.Certificate.PairSemantics.raw9034step1 line 265
  51. def OAI.MUB6.Certificate.PairSemantics.raw9034step2 line 267
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical9034 line 269
  53. def OAI.MUB6.Certificate.PairSemantics.raw9035 line 288
  54. def OAI.MUB6.Certificate.PairSemantics.raw9035step0 line 290
  55. def OAI.MUB6.Certificate.PairSemantics.raw9035step1 line 292
  56. def OAI.MUB6.Certificate.PairSemantics.raw9035step2 line 294
  57. def OAI.MUB6.Certificate.PairSemantics.raw9035step3 line 296
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical9035 line 298
  59. def OAI.MUB6.Certificate.PairSemantics.raw9036 line 323
  60. def OAI.MUB6.Certificate.PairSemantics.raw9036step0 line 325
  61. def OAI.MUB6.Certificate.PairSemantics.raw9036step1 line 327
  62. def OAI.MUB6.Certificate.PairSemantics.raw9036step2 line 329
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical9036 line 331
  64. def OAI.MUB6.Certificate.PairSemantics.raw9037 line 351
  65. def OAI.MUB6.Certificate.PairSemantics.raw9037step0 line 353
  66. def OAI.MUB6.Certificate.PairSemantics.raw9037step1 line 355
  67. def OAI.MUB6.Certificate.PairSemantics.raw9037step2 line 357
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical9037 line 359
  69. def OAI.MUB6.Certificate.PairSemantics.raw9038 line 378
  70. def OAI.MUB6.Certificate.PairSemantics.raw9038step0 line 380
  71. def OAI.MUB6.Certificate.PairSemantics.raw9038step1 line 382
  72. def OAI.MUB6.Certificate.PairSemantics.raw9038step2 line 384
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical9038 line 386
  74. def OAI.MUB6.Certificate.PairSemantics.raw9039 line 406
  75. def OAI.MUB6.Certificate.PairSemantics.raw9039step0 line 408
  76. def OAI.MUB6.Certificate.PairSemantics.raw9039step1 line 410
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical9039 line 412
  78. def OAI.MUB6.Certificate.PairSemantics.raw9040 line 427
  79. def OAI.MUB6.Certificate.PairSemantics.raw9040step0 line 429
  80. def OAI.MUB6.Certificate.PairSemantics.raw9040step1 line 431
  81. def OAI.MUB6.Certificate.PairSemantics.raw9040step2 line 433
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical9040 line 435
  83. def OAI.MUB6.Certificate.PairSemantics.raw9041 line 455
  84. def OAI.MUB6.Certificate.PairSemantics.raw9041step0 line 457
  85. def OAI.MUB6.Certificate.PairSemantics.raw9041step1 line 459
  86. def OAI.MUB6.Certificate.PairSemantics.raw9041step2 line 461
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical9041 line 463
  88. def OAI.MUB6.Certificate.PairSemantics.raw9042 line 483
  89. def OAI.MUB6.Certificate.PairSemantics.raw9042step0 line 485
  90. def OAI.MUB6.Certificate.PairSemantics.raw9042step1 line 487
  91. def OAI.MUB6.Certificate.PairSemantics.raw9042step2 line 489
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical9042 line 491
  93. def OAI.MUB6.Certificate.PairSemantics.raw9043 line 510
  94. def OAI.MUB6.Certificate.PairSemantics.raw9043step0 line 512
  95. def OAI.MUB6.Certificate.PairSemantics.raw9043step1 line 514
  96. def OAI.MUB6.Certificate.PairSemantics.raw9043step2 line 516
  97. def OAI.MUB6.Certificate.PairSemantics.raw9043step3 line 518
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical9043 line 520
  99. def OAI.MUB6.Certificate.PairSemantics.raw9044 line 544
  100. def OAI.MUB6.Certificate.PairSemantics.raw9044step0 line 546
  101. def OAI.MUB6.Certificate.PairSemantics.raw9044step1 line 548
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical9044 line 550
  103. def OAI.MUB6.Certificate.PairSemantics.raw9045 line 565
  104. def OAI.MUB6.Certificate.PairSemantics.raw9045step0 line 567
  105. def OAI.MUB6.Certificate.PairSemantics.raw9045step1 line 569
  106. def OAI.MUB6.Certificate.PairSemantics.raw9045step2 line 571
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical9045 line 573
  108. def OAI.MUB6.Certificate.PairSemantics.raw9046 line 592
  109. def OAI.MUB6.Certificate.PairSemantics.raw9046step0 line 594
  110. def OAI.MUB6.Certificate.PairSemantics.raw9046step1 line 596
  111. def OAI.MUB6.Certificate.PairSemantics.raw9046step2 line 598
  112. def OAI.MUB6.Certificate.PairSemantics.raw9046step3 line 600
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical9046 line 602
  114. def OAI.MUB6.Certificate.PairSemantics.raw9047 line 626
  115. def OAI.MUB6.Certificate.PairSemantics.raw9047step0 line 628
  116. def OAI.MUB6.Certificate.PairSemantics.raw9047step1 line 630
  117. def OAI.MUB6.Certificate.PairSemantics.raw9047step2 line 632
  118. def OAI.MUB6.Certificate.PairSemantics.raw9047step3 line 634
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical9047 line 636
  120. def OAI.MUB6.Certificate.PairSemantics.raw9048 line 660
  121. def OAI.MUB6.Certificate.PairSemantics.raw9048step0 line 662
  122. def OAI.MUB6.Certificate.PairSemantics.raw9048step1 line 664
  123. def OAI.MUB6.Certificate.PairSemantics.raw9048step2 line 666
  124. theorem OAI.MUB6.Certificate.PairSemantics.canonical9048 line 668
  125. def OAI.MUB6.Certificate.PairSemantics.raw9049 line 688
  126. def OAI.MUB6.Certificate.PairSemantics.raw9049step0 line 690
  127. def OAI.MUB6.Certificate.PairSemantics.raw9049step1 line 692
  128. theorem OAI.MUB6.Certificate.PairSemantics.canonical9049 line 694
  129. def OAI.MUB6.Certificate.PairSemantics.raw9050 line 709
  130. def OAI.MUB6.Certificate.PairSemantics.raw9050step0 line 711
  131. def OAI.MUB6.Certificate.PairSemantics.raw9050step1 line 713
  132. def OAI.MUB6.Certificate.PairSemantics.raw9050step2 line 715
  133. theorem OAI.MUB6.Certificate.PairSemantics.canonical9050 line 717
  134. def OAI.MUB6.Certificate.PairSemantics.raw9051 line 736
  135. def OAI.MUB6.Certificate.PairSemantics.raw9051step0 line 738
  136. def OAI.MUB6.Certificate.PairSemantics.raw9051step1 line 740
  137. def OAI.MUB6.Certificate.PairSemantics.raw9051step2 line 742
  138. theorem OAI.MUB6.Certificate.PairSemantics.canonical9051 line 744
  139. def OAI.MUB6.Certificate.PairSemantics.raw9052 line 764
  140. def OAI.MUB6.Certificate.PairSemantics.raw9052step0 line 766
  141. def OAI.MUB6.Certificate.PairSemantics.raw9052step1 line 768
  142. def OAI.MUB6.Certificate.PairSemantics.raw9052step2 line 770
  143. def OAI.MUB6.Certificate.PairSemantics.raw9052step3 line 772
  144. theorem OAI.MUB6.Certificate.PairSemantics.canonical9052 line 774
  145. def OAI.MUB6.Certificate.PairSemantics.raw9053 line 799
  146. def OAI.MUB6.Certificate.PairSemantics.raw9053step0 line 801
  147. def OAI.MUB6.Certificate.PairSemantics.raw9053step1 line 803
  148. def OAI.MUB6.Certificate.PairSemantics.raw9053step2 line 805
  149. theorem OAI.MUB6.Certificate.PairSemantics.canonical9053 line 807
  150. def OAI.MUB6.Certificate.PairSemantics.raw9054 line 826
  151. def OAI.MUB6.Certificate.PairSemantics.raw9054step0 line 828
  152. def OAI.MUB6.Certificate.PairSemantics.raw9054step1 line 830
  153. def OAI.MUB6.Certificate.PairSemantics.raw9054step2 line 832
  154. theorem OAI.MUB6.Certificate.PairSemantics.canonical9054 line 834
  155. def OAI.MUB6.Certificate.PairSemantics.raw9055 line 854
  156. def OAI.MUB6.Certificate.PairSemantics.raw9055step0 line 856
  157. def OAI.MUB6.Certificate.PairSemantics.raw9055step1 line 858
  158. def OAI.MUB6.Certificate.PairSemantics.raw9055step2 line 860
  159. def OAI.MUB6.Certificate.PairSemantics.raw9055step3 line 862
  160. def OAI.MUB6.Certificate.PairSemantics.raw9055step4 line 864
  161. def OAI.MUB6.Certificate.PairSemantics.raw9055step5 line 866
  162. def OAI.MUB6.Certificate.PairSemantics.raw9055step6 line 868
  163. theorem OAI.MUB6.Certificate.PairSemantics.canonical9055 line 870