OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical317.lean

GitHub source file

130 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw10144 line 11
  2. def OAI.MUB6.Certificate.PairSemantics.raw10144step0 line 13
  3. def OAI.MUB6.Certificate.PairSemantics.raw10144step1 line 15
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical10144 line 17
  5. def OAI.MUB6.Certificate.PairSemantics.raw10145 line 30
  6. def OAI.MUB6.Certificate.PairSemantics.raw10145step0 line 32
  7. def OAI.MUB6.Certificate.PairSemantics.raw10145step1 line 34
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical10145 line 36
  9. def OAI.MUB6.Certificate.PairSemantics.raw10146 line 49
  10. def OAI.MUB6.Certificate.PairSemantics.raw10146step0 line 51
  11. def OAI.MUB6.Certificate.PairSemantics.raw10146step1 line 53
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical10146 line 55
  13. def OAI.MUB6.Certificate.PairSemantics.raw10147 line 68
  14. def OAI.MUB6.Certificate.PairSemantics.raw10147step0 line 70
  15. def OAI.MUB6.Certificate.PairSemantics.raw10147step1 line 72
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical10147 line 74
  17. def OAI.MUB6.Certificate.PairSemantics.raw10148 line 87
  18. def OAI.MUB6.Certificate.PairSemantics.raw10148step0 line 89
  19. def OAI.MUB6.Certificate.PairSemantics.raw10148step1 line 91
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical10148 line 93
  21. def OAI.MUB6.Certificate.PairSemantics.raw10149 line 106
  22. def OAI.MUB6.Certificate.PairSemantics.raw10149step0 line 108
  23. def OAI.MUB6.Certificate.PairSemantics.raw10149step1 line 110
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical10149 line 112
  25. def OAI.MUB6.Certificate.PairSemantics.raw10150 line 125
  26. def OAI.MUB6.Certificate.PairSemantics.raw10150step0 line 127
  27. def OAI.MUB6.Certificate.PairSemantics.raw10150step1 line 129
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical10150 line 131
  29. def OAI.MUB6.Certificate.PairSemantics.raw10151 line 144
  30. def OAI.MUB6.Certificate.PairSemantics.raw10151step0 line 146
  31. def OAI.MUB6.Certificate.PairSemantics.raw10151step1 line 148
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical10151 line 150
  33. def OAI.MUB6.Certificate.PairSemantics.raw10152 line 163
  34. def OAI.MUB6.Certificate.PairSemantics.raw10152step0 line 165
  35. def OAI.MUB6.Certificate.PairSemantics.raw10152step1 line 167
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical10152 line 169
  37. def OAI.MUB6.Certificate.PairSemantics.raw10153 line 182
  38. def OAI.MUB6.Certificate.PairSemantics.raw10153step0 line 184
  39. def OAI.MUB6.Certificate.PairSemantics.raw10153step1 line 186
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical10153 line 188
  41. def OAI.MUB6.Certificate.PairSemantics.raw10154 line 201
  42. def OAI.MUB6.Certificate.PairSemantics.raw10154step0 line 203
  43. def OAI.MUB6.Certificate.PairSemantics.raw10154step1 line 205
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical10154 line 207
  45. def OAI.MUB6.Certificate.PairSemantics.raw10155 line 220
  46. def OAI.MUB6.Certificate.PairSemantics.raw10155step0 line 222
  47. def OAI.MUB6.Certificate.PairSemantics.raw10155step1 line 224
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical10155 line 226
  49. def OAI.MUB6.Certificate.PairSemantics.raw10156 line 239
  50. def OAI.MUB6.Certificate.PairSemantics.raw10156step0 line 241
  51. def OAI.MUB6.Certificate.PairSemantics.raw10156step1 line 243
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical10156 line 245
  53. def OAI.MUB6.Certificate.PairSemantics.raw10157 line 258
  54. def OAI.MUB6.Certificate.PairSemantics.raw10157step0 line 260
  55. def OAI.MUB6.Certificate.PairSemantics.raw10157step1 line 262
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical10157 line 264
  57. def OAI.MUB6.Certificate.PairSemantics.raw10158 line 277
  58. def OAI.MUB6.Certificate.PairSemantics.raw10158step0 line 279
  59. def OAI.MUB6.Certificate.PairSemantics.raw10158step1 line 281
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical10158 line 283
  61. def OAI.MUB6.Certificate.PairSemantics.raw10159 line 296
  62. def OAI.MUB6.Certificate.PairSemantics.raw10159step0 line 298
  63. def OAI.MUB6.Certificate.PairSemantics.raw10159step1 line 300
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical10159 line 302
  65. def OAI.MUB6.Certificate.PairSemantics.raw10160 line 315
  66. def OAI.MUB6.Certificate.PairSemantics.raw10160step0 line 317
  67. def OAI.MUB6.Certificate.PairSemantics.raw10160step1 line 319
  68. def OAI.MUB6.Certificate.PairSemantics.raw10160step2 line 321
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical10160 line 323
  70. def OAI.MUB6.Certificate.PairSemantics.raw10161 line 340
  71. def OAI.MUB6.Certificate.PairSemantics.raw10161step0 line 342
  72. def OAI.MUB6.Certificate.PairSemantics.raw10161step1 line 344
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical10161 line 346
  74. def OAI.MUB6.Certificate.PairSemantics.raw10162 line 359
  75. def OAI.MUB6.Certificate.PairSemantics.raw10162step0 line 361
  76. def OAI.MUB6.Certificate.PairSemantics.raw10162step1 line 363
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical10162 line 365
  78. def OAI.MUB6.Certificate.PairSemantics.raw10163 line 378
  79. def OAI.MUB6.Certificate.PairSemantics.raw10163step0 line 380
  80. def OAI.MUB6.Certificate.PairSemantics.raw10163step1 line 382
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical10163 line 384
  82. def OAI.MUB6.Certificate.PairSemantics.raw10164 line 397
  83. def OAI.MUB6.Certificate.PairSemantics.raw10164step0 line 399
  84. def OAI.MUB6.Certificate.PairSemantics.raw10164step1 line 401
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical10164 line 403
  86. def OAI.MUB6.Certificate.PairSemantics.raw10165 line 416
  87. def OAI.MUB6.Certificate.PairSemantics.raw10165step0 line 418
  88. def OAI.MUB6.Certificate.PairSemantics.raw10165step1 line 420
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical10165 line 422
  90. def OAI.MUB6.Certificate.PairSemantics.raw10166 line 435
  91. def OAI.MUB6.Certificate.PairSemantics.raw10166step0 line 437
  92. def OAI.MUB6.Certificate.PairSemantics.raw10166step1 line 439
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical10166 line 441
  94. def OAI.MUB6.Certificate.PairSemantics.raw10167 line 454
  95. def OAI.MUB6.Certificate.PairSemantics.raw10167step0 line 456
  96. def OAI.MUB6.Certificate.PairSemantics.raw10167step1 line 458
  97. def OAI.MUB6.Certificate.PairSemantics.raw10167step2 line 460
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical10167 line 462
  99. def OAI.MUB6.Certificate.PairSemantics.raw10168 line 479
  100. def OAI.MUB6.Certificate.PairSemantics.raw10168step0 line 481
  101. def OAI.MUB6.Certificate.PairSemantics.raw10168step1 line 483
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical10168 line 485
  103. def OAI.MUB6.Certificate.PairSemantics.raw10169 line 498
  104. def OAI.MUB6.Certificate.PairSemantics.raw10169step0 line 500
  105. def OAI.MUB6.Certificate.PairSemantics.raw10169step1 line 502
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical10169 line 504
  107. def OAI.MUB6.Certificate.PairSemantics.raw10170 line 517
  108. def OAI.MUB6.Certificate.PairSemantics.raw10170step0 line 519
  109. def OAI.MUB6.Certificate.PairSemantics.raw10170step1 line 521
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical10170 line 523
  111. def OAI.MUB6.Certificate.PairSemantics.raw10171 line 536
  112. def OAI.MUB6.Certificate.PairSemantics.raw10171step0 line 538
  113. def OAI.MUB6.Certificate.PairSemantics.raw10171step1 line 540
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical10171 line 542
  115. def OAI.MUB6.Certificate.PairSemantics.raw10172 line 555
  116. def OAI.MUB6.Certificate.PairSemantics.raw10172step0 line 557
  117. def OAI.MUB6.Certificate.PairSemantics.raw10172step1 line 559
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical10172 line 561
  119. def OAI.MUB6.Certificate.PairSemantics.raw10173 line 574
  120. def OAI.MUB6.Certificate.PairSemantics.raw10173step0 line 576
  121. def OAI.MUB6.Certificate.PairSemantics.raw10173step1 line 578
  122. theorem OAI.MUB6.Certificate.PairSemantics.canonical10173 line 580
  123. def OAI.MUB6.Certificate.PairSemantics.raw10174 line 593
  124. def OAI.MUB6.Certificate.PairSemantics.raw10174step0 line 595
  125. def OAI.MUB6.Certificate.PairSemantics.raw10174step1 line 597
  126. theorem OAI.MUB6.Certificate.PairSemantics.canonical10174 line 599
  127. def OAI.MUB6.Certificate.PairSemantics.raw10175 line 612
  128. def OAI.MUB6.Certificate.PairSemantics.raw10175step0 line 614
  129. def OAI.MUB6.Certificate.PairSemantics.raw10175step1 line 616
  130. theorem OAI.MUB6.Certificate.PairSemantics.canonical10175 line 618