OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical249.lean

GitHub source file

128 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7968 line 15
  2. def OAI.MUB6.Certificate.PairSemantics.raw7968step0 line 17
  3. def OAI.MUB6.Certificate.PairSemantics.raw7968step1 line 19
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7968 line 21
  5. def OAI.MUB6.Certificate.PairSemantics.raw7969 line 34
  6. def OAI.MUB6.Certificate.PairSemantics.raw7969step0 line 36
  7. def OAI.MUB6.Certificate.PairSemantics.raw7969step1 line 38
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical7969 line 40
  9. def OAI.MUB6.Certificate.PairSemantics.raw7970 line 53
  10. def OAI.MUB6.Certificate.PairSemantics.raw7970step0 line 55
  11. def OAI.MUB6.Certificate.PairSemantics.raw7970step1 line 57
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical7970 line 59
  13. def OAI.MUB6.Certificate.PairSemantics.raw7971 line 72
  14. def OAI.MUB6.Certificate.PairSemantics.raw7971step0 line 74
  15. def OAI.MUB6.Certificate.PairSemantics.raw7971step1 line 76
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical7971 line 78
  17. def OAI.MUB6.Certificate.PairSemantics.raw7972 line 91
  18. def OAI.MUB6.Certificate.PairSemantics.raw7972step0 line 93
  19. def OAI.MUB6.Certificate.PairSemantics.raw7972step1 line 95
  20. theorem OAI.MUB6.Certificate.PairSemantics.canonical7972 line 97
  21. def OAI.MUB6.Certificate.PairSemantics.raw7973 line 110
  22. def OAI.MUB6.Certificate.PairSemantics.raw7973step0 line 112
  23. def OAI.MUB6.Certificate.PairSemantics.raw7973step1 line 114
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical7973 line 116
  25. def OAI.MUB6.Certificate.PairSemantics.raw7974 line 129
  26. def OAI.MUB6.Certificate.PairSemantics.raw7974step0 line 131
  27. def OAI.MUB6.Certificate.PairSemantics.raw7974step1 line 133
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical7974 line 135
  29. def OAI.MUB6.Certificate.PairSemantics.raw7975 line 148
  30. def OAI.MUB6.Certificate.PairSemantics.raw7975step0 line 150
  31. def OAI.MUB6.Certificate.PairSemantics.raw7975step1 line 152
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical7975 line 154
  33. def OAI.MUB6.Certificate.PairSemantics.raw7976 line 167
  34. def OAI.MUB6.Certificate.PairSemantics.raw7976step0 line 169
  35. def OAI.MUB6.Certificate.PairSemantics.raw7976step1 line 171
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical7976 line 173
  37. def OAI.MUB6.Certificate.PairSemantics.raw7977 line 186
  38. def OAI.MUB6.Certificate.PairSemantics.raw7977step0 line 188
  39. def OAI.MUB6.Certificate.PairSemantics.raw7977step1 line 190
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical7977 line 192
  41. def OAI.MUB6.Certificate.PairSemantics.raw7978 line 205
  42. def OAI.MUB6.Certificate.PairSemantics.raw7978step0 line 207
  43. def OAI.MUB6.Certificate.PairSemantics.raw7978step1 line 209
  44. def OAI.MUB6.Certificate.PairSemantics.raw7978step2 line 211
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical7978 line 213
  46. def OAI.MUB6.Certificate.PairSemantics.raw7979 line 233
  47. def OAI.MUB6.Certificate.PairSemantics.raw7979step0 line 235
  48. def OAI.MUB6.Certificate.PairSemantics.raw7979step1 line 237
  49. def OAI.MUB6.Certificate.PairSemantics.raw7979step2 line 239
  50. def OAI.MUB6.Certificate.PairSemantics.raw7979step3 line 241
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical7979 line 243
  52. def OAI.MUB6.Certificate.PairSemantics.raw7980 line 268
  53. def OAI.MUB6.Certificate.PairSemantics.raw7980step0 line 270
  54. def OAI.MUB6.Certificate.PairSemantics.raw7980step1 line 272
  55. def OAI.MUB6.Certificate.PairSemantics.raw7980step2 line 274
  56. def OAI.MUB6.Certificate.PairSemantics.raw7980step3 line 276
  57. def OAI.MUB6.Certificate.PairSemantics.raw7980step4 line 278
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical7980 line 280
  59. def OAI.MUB6.Certificate.PairSemantics.raw7981 line 310
  60. def OAI.MUB6.Certificate.PairSemantics.raw7981step0 line 312
  61. def OAI.MUB6.Certificate.PairSemantics.raw7981step1 line 314
  62. def OAI.MUB6.Certificate.PairSemantics.raw7981step2 line 316
  63. def OAI.MUB6.Certificate.PairSemantics.raw7981step3 line 318
  64. def OAI.MUB6.Certificate.PairSemantics.raw7981step4 line 320
  65. def OAI.MUB6.Certificate.PairSemantics.raw7981step5 line 322
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical7981 line 324
  67. def OAI.MUB6.Certificate.PairSemantics.raw7982 line 359
  68. def OAI.MUB6.Certificate.PairSemantics.raw7982step0 line 361
  69. def OAI.MUB6.Certificate.PairSemantics.raw7982step1 line 363
  70. def OAI.MUB6.Certificate.PairSemantics.raw7982step2 line 365
  71. def OAI.MUB6.Certificate.PairSemantics.raw7982step3 line 367
  72. def OAI.MUB6.Certificate.PairSemantics.raw7982step4 line 369
  73. def OAI.MUB6.Certificate.PairSemantics.raw7982step5 line 371
  74. def OAI.MUB6.Certificate.PairSemantics.raw7982step6 line 373
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical7982 line 375
  76. def OAI.MUB6.Certificate.PairSemantics.raw7983 line 415
  77. def OAI.MUB6.Certificate.PairSemantics.raw7983step0 line 417
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical7983 line 419
  79. def OAI.MUB6.Certificate.PairSemantics.raw7984 line 428
  80. def OAI.MUB6.Certificate.PairSemantics.raw7984step0 line 430
  81. def OAI.MUB6.Certificate.PairSemantics.raw7984step1 line 432
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical7984 line 434
  83. def OAI.MUB6.Certificate.PairSemantics.raw7985 line 447
  84. def OAI.MUB6.Certificate.PairSemantics.raw7985step0 line 449
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical7985 line 451
  86. def OAI.MUB6.Certificate.PairSemantics.raw7986 line 460
  87. def OAI.MUB6.Certificate.PairSemantics.raw7986step0 line 462
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical7986 line 464
  89. def OAI.MUB6.Certificate.PairSemantics.raw7987 line 473
  90. def OAI.MUB6.Certificate.PairSemantics.raw7987step0 line 475
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical7987 line 477
  92. def OAI.MUB6.Certificate.PairSemantics.raw7988 line 487
  93. def OAI.MUB6.Certificate.PairSemantics.raw7988step0 line 489
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical7988 line 491
  95. def OAI.MUB6.Certificate.PairSemantics.raw7989 line 501
  96. def OAI.MUB6.Certificate.PairSemantics.raw7989step0 line 503
  97. def OAI.MUB6.Certificate.PairSemantics.raw7989step1 line 505
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical7989 line 507
  99. def OAI.MUB6.Certificate.PairSemantics.raw7990 line 520
  100. def OAI.MUB6.Certificate.PairSemantics.raw7990step0 line 522
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical7990 line 524
  102. def OAI.MUB6.Certificate.PairSemantics.raw7991 line 533
  103. def OAI.MUB6.Certificate.PairSemantics.raw7991step0 line 535
  104. theorem OAI.MUB6.Certificate.PairSemantics.canonical7991 line 537
  105. def OAI.MUB6.Certificate.PairSemantics.raw7992 line 546
  106. def OAI.MUB6.Certificate.PairSemantics.raw7992step0 line 548
  107. theorem OAI.MUB6.Certificate.PairSemantics.canonical7992 line 550
  108. def OAI.MUB6.Certificate.PairSemantics.raw7993 line 559
  109. def OAI.MUB6.Certificate.PairSemantics.raw7993step0 line 561
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical7993 line 563
  111. def OAI.MUB6.Certificate.PairSemantics.raw7994 line 572
  112. def OAI.MUB6.Certificate.PairSemantics.raw7994step0 line 574
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical7994 line 576
  114. def OAI.MUB6.Certificate.PairSemantics.raw7995 line 585
  115. def OAI.MUB6.Certificate.PairSemantics.raw7995step0 line 587
  116. theorem OAI.MUB6.Certificate.PairSemantics.canonical7995 line 589
  117. def OAI.MUB6.Certificate.PairSemantics.raw7996 line 598
  118. def OAI.MUB6.Certificate.PairSemantics.raw7996step0 line 600
  119. theorem OAI.MUB6.Certificate.PairSemantics.canonical7996 line 602
  120. def OAI.MUB6.Certificate.PairSemantics.raw7997 line 611
  121. def OAI.MUB6.Certificate.PairSemantics.raw7997step0 line 613
  122. theorem OAI.MUB6.Certificate.PairSemantics.canonical7997 line 615
  123. def OAI.MUB6.Certificate.PairSemantics.raw7998 line 624
  124. def OAI.MUB6.Certificate.PairSemantics.raw7998step0 line 626
  125. theorem OAI.MUB6.Certificate.PairSemantics.canonical7998 line 628
  126. def OAI.MUB6.Certificate.PairSemantics.raw7999 line 637
  127. def OAI.MUB6.Certificate.PairSemantics.raw7999step0 line 639
  128. theorem OAI.MUB6.Certificate.PairSemantics.canonical7999 line 641