OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical312.lean

GitHub source file

129 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw9984 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw9984step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw9984step1 line 23
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical9984 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw9985 line 39
  6. def OAI.MUB6.Certificate.PairSemantics.raw9985step0 line 41
  7. def OAI.MUB6.Certificate.PairSemantics.raw9985step1 line 43
  8. def OAI.MUB6.Certificate.PairSemantics.raw9985step2 line 45
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical9985 line 47
  10. def OAI.MUB6.Certificate.PairSemantics.raw9986 line 64
  11. def OAI.MUB6.Certificate.PairSemantics.raw9986step0 line 66
  12. def OAI.MUB6.Certificate.PairSemantics.raw9986step1 line 68
  13. def OAI.MUB6.Certificate.PairSemantics.raw9986step2 line 70
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical9986 line 72
  15. def OAI.MUB6.Certificate.PairSemantics.raw9987 line 89
  16. def OAI.MUB6.Certificate.PairSemantics.raw9987step0 line 91
  17. def OAI.MUB6.Certificate.PairSemantics.raw9987step1 line 93
  18. def OAI.MUB6.Certificate.PairSemantics.raw9987step2 line 95
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical9987 line 97
  20. def OAI.MUB6.Certificate.PairSemantics.raw9988 line 114
  21. def OAI.MUB6.Certificate.PairSemantics.raw9988step0 line 116
  22. def OAI.MUB6.Certificate.PairSemantics.raw9988step1 line 118
  23. def OAI.MUB6.Certificate.PairSemantics.raw9988step2 line 120
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical9988 line 122
  25. def OAI.MUB6.Certificate.PairSemantics.raw9989 line 139
  26. def OAI.MUB6.Certificate.PairSemantics.raw9989step0 line 141
  27. def OAI.MUB6.Certificate.PairSemantics.raw9989step1 line 143
  28. def OAI.MUB6.Certificate.PairSemantics.raw9989step2 line 145
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical9989 line 147
  30. def OAI.MUB6.Certificate.PairSemantics.raw9990 line 164
  31. def OAI.MUB6.Certificate.PairSemantics.raw9990step0 line 166
  32. def OAI.MUB6.Certificate.PairSemantics.raw9990step1 line 168
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical9990 line 170
  34. def OAI.MUB6.Certificate.PairSemantics.raw9991 line 183
  35. def OAI.MUB6.Certificate.PairSemantics.raw9991step0 line 185
  36. def OAI.MUB6.Certificate.PairSemantics.raw9991step1 line 187
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical9991 line 189
  38. def OAI.MUB6.Certificate.PairSemantics.raw9992 line 202
  39. def OAI.MUB6.Certificate.PairSemantics.raw9992step0 line 204
  40. def OAI.MUB6.Certificate.PairSemantics.raw9992step1 line 206
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical9992 line 208
  42. def OAI.MUB6.Certificate.PairSemantics.raw9993 line 221
  43. def OAI.MUB6.Certificate.PairSemantics.raw9993step0 line 223
  44. def OAI.MUB6.Certificate.PairSemantics.raw9993step1 line 225
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical9993 line 227
  46. def OAI.MUB6.Certificate.PairSemantics.raw9994 line 240
  47. def OAI.MUB6.Certificate.PairSemantics.raw9994step0 line 242
  48. def OAI.MUB6.Certificate.PairSemantics.raw9994step1 line 244
  49. def OAI.MUB6.Certificate.PairSemantics.raw9994step2 line 246
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical9994 line 248
  51. def OAI.MUB6.Certificate.PairSemantics.raw9995 line 265
  52. def OAI.MUB6.Certificate.PairSemantics.raw9995step0 line 267
  53. def OAI.MUB6.Certificate.PairSemantics.raw9995step1 line 269
  54. def OAI.MUB6.Certificate.PairSemantics.raw9995step2 line 271
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical9995 line 273
  56. def OAI.MUB6.Certificate.PairSemantics.raw9996 line 291
  57. def OAI.MUB6.Certificate.PairSemantics.raw9996step0 line 293
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical9996 line 295
  59. def OAI.MUB6.Certificate.PairSemantics.raw9997 line 304
  60. def OAI.MUB6.Certificate.PairSemantics.raw9997step0 line 306
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical9997 line 308
  62. def OAI.MUB6.Certificate.PairSemantics.raw9998 line 317
  63. def OAI.MUB6.Certificate.PairSemantics.raw9998step0 line 319
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical9998 line 321
  65. def OAI.MUB6.Certificate.PairSemantics.raw9999 line 330
  66. def OAI.MUB6.Certificate.PairSemantics.raw9999step0 line 332
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical9999 line 334
  68. def OAI.MUB6.Certificate.PairSemantics.raw10000 line 343
  69. def OAI.MUB6.Certificate.PairSemantics.raw10000step0 line 345
  70. def OAI.MUB6.Certificate.PairSemantics.raw10000step1 line 347
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical10000 line 349
  72. def OAI.MUB6.Certificate.PairSemantics.raw10001 line 363
  73. def OAI.MUB6.Certificate.PairSemantics.raw10001step0 line 365
  74. def OAI.MUB6.Certificate.PairSemantics.raw10001step1 line 367
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical10001 line 369
  76. def OAI.MUB6.Certificate.PairSemantics.raw10002 line 383
  77. def OAI.MUB6.Certificate.PairSemantics.raw10002step0 line 385
  78. def OAI.MUB6.Certificate.PairSemantics.raw10002step1 line 387
  79. theorem OAI.MUB6.Certificate.PairSemantics.canonical10002 line 389
  80. def OAI.MUB6.Certificate.PairSemantics.raw10003 line 403
  81. def OAI.MUB6.Certificate.PairSemantics.raw10003step0 line 405
  82. def OAI.MUB6.Certificate.PairSemantics.raw10003step1 line 407
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical10003 line 409
  84. def OAI.MUB6.Certificate.PairSemantics.raw10004 line 423
  85. def OAI.MUB6.Certificate.PairSemantics.raw10004step0 line 425
  86. def OAI.MUB6.Certificate.PairSemantics.raw10004step1 line 427
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical10004 line 429
  88. def OAI.MUB6.Certificate.PairSemantics.raw10005 line 443
  89. def OAI.MUB6.Certificate.PairSemantics.raw10005step0 line 445
  90. def OAI.MUB6.Certificate.PairSemantics.raw10005step1 line 447
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical10005 line 449
  92. def OAI.MUB6.Certificate.PairSemantics.raw10006 line 463
  93. def OAI.MUB6.Certificate.PairSemantics.raw10006step0 line 465
  94. def OAI.MUB6.Certificate.PairSemantics.raw10006step1 line 467
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical10006 line 469
  96. def OAI.MUB6.Certificate.PairSemantics.raw10007 line 483
  97. def OAI.MUB6.Certificate.PairSemantics.raw10007step0 line 485
  98. def OAI.MUB6.Certificate.PairSemantics.raw10007step1 line 487
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical10007 line 489
  100. def OAI.MUB6.Certificate.PairSemantics.raw10008 line 503
  101. def OAI.MUB6.Certificate.PairSemantics.raw10008step0 line 505
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical10008 line 507
  103. def OAI.MUB6.Certificate.PairSemantics.raw10009 line 516
  104. def OAI.MUB6.Certificate.PairSemantics.raw10009step0 line 518
  105. def OAI.MUB6.Certificate.PairSemantics.raw10009step1 line 520
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical10009 line 522
  107. def OAI.MUB6.Certificate.PairSemantics.raw10010 line 536
  108. def OAI.MUB6.Certificate.PairSemantics.raw10010step0 line 538
  109. def OAI.MUB6.Certificate.PairSemantics.raw10010step1 line 540
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical10010 line 542
  111. def OAI.MUB6.Certificate.PairSemantics.raw10011 line 556
  112. def OAI.MUB6.Certificate.PairSemantics.raw10011step0 line 558
  113. def OAI.MUB6.Certificate.PairSemantics.raw10011step1 line 560
  114. theorem OAI.MUB6.Certificate.PairSemantics.canonical10011 line 562
  115. def OAI.MUB6.Certificate.PairSemantics.raw10012 line 576
  116. def OAI.MUB6.Certificate.PairSemantics.raw10012step0 line 578
  117. def OAI.MUB6.Certificate.PairSemantics.raw10012step1 line 580
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical10012 line 582
  119. def OAI.MUB6.Certificate.PairSemantics.raw10013 line 596
  120. def OAI.MUB6.Certificate.PairSemantics.raw10013step0 line 598
  121. def OAI.MUB6.Certificate.PairSemantics.raw10013step1 line 600
  122. theorem OAI.MUB6.Certificate.PairSemantics.canonical10013 line 602
  123. def OAI.MUB6.Certificate.PairSemantics.raw10014 line 616
  124. def OAI.MUB6.Certificate.PairSemantics.raw10014step0 line 618
  125. def OAI.MUB6.Certificate.PairSemantics.raw10014step1 line 620
  126. theorem OAI.MUB6.Certificate.PairSemantics.canonical10014 line 622
  127. def OAI.MUB6.Certificate.PairSemantics.raw10015 line 636
  128. def OAI.MUB6.Certificate.PairSemantics.raw10015step0 line 638
  129. theorem OAI.MUB6.Certificate.PairSemantics.canonical10015 line 640