OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical216.lean

GitHub source file

138 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw6912 line 13
  2. def OAI.MUB6.Certificate.PairSemantics.raw6912step0 line 15
  3. def OAI.MUB6.Certificate.PairSemantics.raw6912step1 line 17
  4. def OAI.MUB6.Certificate.PairSemantics.raw6912step2 line 19
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical6912 line 21
  6. def OAI.MUB6.Certificate.PairSemantics.raw6913 line 38
  7. def OAI.MUB6.Certificate.PairSemantics.raw6913step0 line 40
  8. def OAI.MUB6.Certificate.PairSemantics.raw6913step1 line 42
  9. def OAI.MUB6.Certificate.PairSemantics.raw6913step2 line 44
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical6913 line 46
  11. def OAI.MUB6.Certificate.PairSemantics.raw6914 line 63
  12. def OAI.MUB6.Certificate.PairSemantics.raw6914step0 line 65
  13. def OAI.MUB6.Certificate.PairSemantics.raw6914step1 line 67
  14. def OAI.MUB6.Certificate.PairSemantics.raw6914step2 line 69
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical6914 line 71
  16. def OAI.MUB6.Certificate.PairSemantics.raw6915 line 88
  17. def OAI.MUB6.Certificate.PairSemantics.raw6915step0 line 90
  18. def OAI.MUB6.Certificate.PairSemantics.raw6915step1 line 92
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical6915 line 94
  20. def OAI.MUB6.Certificate.PairSemantics.raw6916 line 107
  21. def OAI.MUB6.Certificate.PairSemantics.raw6916step0 line 109
  22. def OAI.MUB6.Certificate.PairSemantics.raw6916step1 line 111
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical6916 line 113
  24. def OAI.MUB6.Certificate.PairSemantics.raw6917 line 126
  25. def OAI.MUB6.Certificate.PairSemantics.raw6917step0 line 128
  26. def OAI.MUB6.Certificate.PairSemantics.raw6917step1 line 130
  27. def OAI.MUB6.Certificate.PairSemantics.raw6917step2 line 132
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical6917 line 134
  29. def OAI.MUB6.Certificate.PairSemantics.raw6918 line 151
  30. def OAI.MUB6.Certificate.PairSemantics.raw6918step0 line 153
  31. def OAI.MUB6.Certificate.PairSemantics.raw6918step1 line 155
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical6918 line 157
  33. def OAI.MUB6.Certificate.PairSemantics.raw6919 line 170
  34. def OAI.MUB6.Certificate.PairSemantics.raw6919step0 line 172
  35. def OAI.MUB6.Certificate.PairSemantics.raw6919step1 line 174
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical6919 line 176
  37. def OAI.MUB6.Certificate.PairSemantics.raw6920 line 189
  38. def OAI.MUB6.Certificate.PairSemantics.raw6920step0 line 191
  39. def OAI.MUB6.Certificate.PairSemantics.raw6920step1 line 193
  40. def OAI.MUB6.Certificate.PairSemantics.raw6920step2 line 195
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical6920 line 197
  42. def OAI.MUB6.Certificate.PairSemantics.raw6921 line 214
  43. def OAI.MUB6.Certificate.PairSemantics.raw6921step0 line 216
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical6921 line 218
  45. def OAI.MUB6.Certificate.PairSemantics.raw6922 line 227
  46. def OAI.MUB6.Certificate.PairSemantics.raw6922step0 line 229
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical6922 line 231
  48. def OAI.MUB6.Certificate.PairSemantics.raw6923 line 240
  49. def OAI.MUB6.Certificate.PairSemantics.raw6923step0 line 242
  50. def OAI.MUB6.Certificate.PairSemantics.raw6923step1 line 244
  51. def OAI.MUB6.Certificate.PairSemantics.raw6923step2 line 246
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical6923 line 248
  53. def OAI.MUB6.Certificate.PairSemantics.raw6924 line 265
  54. def OAI.MUB6.Certificate.PairSemantics.raw6924step0 line 267
  55. def OAI.MUB6.Certificate.PairSemantics.raw6924step1 line 269
  56. def OAI.MUB6.Certificate.PairSemantics.raw6924step2 line 271
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical6924 line 273
  58. def OAI.MUB6.Certificate.PairSemantics.raw6925 line 290
  59. def OAI.MUB6.Certificate.PairSemantics.raw6925step0 line 292
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical6925 line 294
  61. def OAI.MUB6.Certificate.PairSemantics.raw6926 line 303
  62. def OAI.MUB6.Certificate.PairSemantics.raw6926step0 line 305
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical6926 line 307
  64. def OAI.MUB6.Certificate.PairSemantics.raw6927 line 316
  65. def OAI.MUB6.Certificate.PairSemantics.raw6927step0 line 318
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical6927 line 320
  67. def OAI.MUB6.Certificate.PairSemantics.raw6928 line 329
  68. def OAI.MUB6.Certificate.PairSemantics.raw6928step0 line 331
  69. def OAI.MUB6.Certificate.PairSemantics.raw6928step1 line 333
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical6928 line 335
  71. def OAI.MUB6.Certificate.PairSemantics.raw6929 line 348
  72. def OAI.MUB6.Certificate.PairSemantics.raw6929step0 line 350
  73. def OAI.MUB6.Certificate.PairSemantics.raw6929step1 line 352
  74. def OAI.MUB6.Certificate.PairSemantics.raw6929step2 line 354
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical6929 line 356
  76. def OAI.MUB6.Certificate.PairSemantics.raw6930 line 373
  77. def OAI.MUB6.Certificate.PairSemantics.raw6930step0 line 375
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical6930 line 377
  79. def OAI.MUB6.Certificate.PairSemantics.raw6931 line 386
  80. def OAI.MUB6.Certificate.PairSemantics.raw6931step0 line 388
  81. def OAI.MUB6.Certificate.PairSemantics.raw6931step1 line 390
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical6931 line 392
  83. def OAI.MUB6.Certificate.PairSemantics.raw6932 line 405
  84. def OAI.MUB6.Certificate.PairSemantics.raw6932step0 line 407
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical6932 line 409
  86. def OAI.MUB6.Certificate.PairSemantics.raw6933 line 418
  87. def OAI.MUB6.Certificate.PairSemantics.raw6933step0 line 420
  88. def OAI.MUB6.Certificate.PairSemantics.raw6933step1 line 422
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical6933 line 424
  90. def OAI.MUB6.Certificate.PairSemantics.raw6934 line 437
  91. def OAI.MUB6.Certificate.PairSemantics.raw6934step0 line 439
  92. def OAI.MUB6.Certificate.PairSemantics.raw6934step1 line 441
  93. def OAI.MUB6.Certificate.PairSemantics.raw6934step2 line 443
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical6934 line 445
  95. def OAI.MUB6.Certificate.PairSemantics.raw6935 line 462
  96. def OAI.MUB6.Certificate.PairSemantics.raw6935step0 line 464
  97. def OAI.MUB6.Certificate.PairSemantics.raw6935step1 line 466
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical6935 line 468
  99. def OAI.MUB6.Certificate.PairSemantics.raw6936 line 481
  100. def OAI.MUB6.Certificate.PairSemantics.raw6936step0 line 483
  101. def OAI.MUB6.Certificate.PairSemantics.raw6936step1 line 485
  102. def OAI.MUB6.Certificate.PairSemantics.raw6936step2 line 487
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical6936 line 489
  104. def OAI.MUB6.Certificate.PairSemantics.raw6937 line 506
  105. def OAI.MUB6.Certificate.PairSemantics.raw6937step0 line 508
  106. def OAI.MUB6.Certificate.PairSemantics.raw6937step1 line 510
  107. def OAI.MUB6.Certificate.PairSemantics.raw6937step2 line 512
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical6937 line 514
  109. def OAI.MUB6.Certificate.PairSemantics.raw6938 line 531
  110. def OAI.MUB6.Certificate.PairSemantics.raw6938step0 line 533
  111. def OAI.MUB6.Certificate.PairSemantics.raw6938step1 line 535
  112. def OAI.MUB6.Certificate.PairSemantics.raw6938step2 line 537
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical6938 line 539
  114. def OAI.MUB6.Certificate.PairSemantics.raw6939 line 556
  115. def OAI.MUB6.Certificate.PairSemantics.raw6939step0 line 558
  116. def OAI.MUB6.Certificate.PairSemantics.raw6939step1 line 560
  117. def OAI.MUB6.Certificate.PairSemantics.raw6939step2 line 562
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical6939 line 564
  119. def OAI.MUB6.Certificate.PairSemantics.raw6940 line 581
  120. def OAI.MUB6.Certificate.PairSemantics.raw6940step0 line 583
  121. def OAI.MUB6.Certificate.PairSemantics.raw6940step1 line 585
  122. def OAI.MUB6.Certificate.PairSemantics.raw6940step2 line 587
  123. theorem OAI.MUB6.Certificate.PairSemantics.canonical6940 line 589
  124. def OAI.MUB6.Certificate.PairSemantics.raw6941 line 606
  125. def OAI.MUB6.Certificate.PairSemantics.raw6941step0 line 608
  126. def OAI.MUB6.Certificate.PairSemantics.raw6941step1 line 610
  127. def OAI.MUB6.Certificate.PairSemantics.raw6941step2 line 612
  128. theorem OAI.MUB6.Certificate.PairSemantics.canonical6941 line 614
  129. def OAI.MUB6.Certificate.PairSemantics.raw6942 line 631
  130. def OAI.MUB6.Certificate.PairSemantics.raw6942step0 line 633
  131. def OAI.MUB6.Certificate.PairSemantics.raw6942step1 line 635
  132. def OAI.MUB6.Certificate.PairSemantics.raw6942step2 line 637
  133. theorem OAI.MUB6.Certificate.PairSemantics.canonical6942 line 639
  134. def OAI.MUB6.Certificate.PairSemantics.raw6943 line 656
  135. def OAI.MUB6.Certificate.PairSemantics.raw6943step0 line 658
  136. def OAI.MUB6.Certificate.PairSemantics.raw6943step1 line 660
  137. def OAI.MUB6.Certificate.PairSemantics.raw6943step2 line 662
  138. theorem OAI.MUB6.Certificate.PairSemantics.canonical6943 line 664