OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical238.lean

GitHub source file

124 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw7616 line 14
  2. def OAI.MUB6.Certificate.PairSemantics.raw7616step0 line 16
  3. def OAI.MUB6.Certificate.PairSemantics.raw7616step1 line 18
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical7616 line 20
  5. def OAI.MUB6.Certificate.PairSemantics.raw7617 line 33
  6. def OAI.MUB6.Certificate.PairSemantics.raw7617step0 line 35
  7. def OAI.MUB6.Certificate.PairSemantics.raw7617step1 line 37
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical7617 line 39
  9. def OAI.MUB6.Certificate.PairSemantics.raw7618 line 52
  10. def OAI.MUB6.Certificate.PairSemantics.raw7618step0 line 54
  11. def OAI.MUB6.Certificate.PairSemantics.raw7618step1 line 56
  12. def OAI.MUB6.Certificate.PairSemantics.raw7618step2 line 58
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical7618 line 60
  14. def OAI.MUB6.Certificate.PairSemantics.raw7619 line 77
  15. def OAI.MUB6.Certificate.PairSemantics.raw7619step0 line 79
  16. def OAI.MUB6.Certificate.PairSemantics.raw7619step1 line 81
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical7619 line 83
  18. def OAI.MUB6.Certificate.PairSemantics.raw7620 line 96
  19. def OAI.MUB6.Certificate.PairSemantics.raw7620step0 line 98
  20. def OAI.MUB6.Certificate.PairSemantics.raw7620step1 line 100
  21. def OAI.MUB6.Certificate.PairSemantics.raw7620step2 line 102
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical7620 line 104
  23. def OAI.MUB6.Certificate.PairSemantics.raw7621 line 121
  24. def OAI.MUB6.Certificate.PairSemantics.raw7621step0 line 123
  25. def OAI.MUB6.Certificate.PairSemantics.raw7621step1 line 125
  26. def OAI.MUB6.Certificate.PairSemantics.raw7621step2 line 127
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical7621 line 129
  28. def OAI.MUB6.Certificate.PairSemantics.raw7622 line 146
  29. def OAI.MUB6.Certificate.PairSemantics.raw7622step0 line 148
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical7622 line 150
  31. def OAI.MUB6.Certificate.PairSemantics.raw7623 line 159
  32. def OAI.MUB6.Certificate.PairSemantics.raw7623step0 line 161
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical7623 line 163
  34. def OAI.MUB6.Certificate.PairSemantics.raw7624 line 172
  35. def OAI.MUB6.Certificate.PairSemantics.raw7624step0 line 174
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical7624 line 176
  37. def OAI.MUB6.Certificate.PairSemantics.raw7625 line 185
  38. def OAI.MUB6.Certificate.PairSemantics.raw7625step0 line 187
  39. def OAI.MUB6.Certificate.PairSemantics.raw7625step1 line 189
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical7625 line 191
  41. def OAI.MUB6.Certificate.PairSemantics.raw7626 line 205
  42. def OAI.MUB6.Certificate.PairSemantics.raw7626step0 line 207
  43. def OAI.MUB6.Certificate.PairSemantics.raw7626step1 line 209
  44. theorem OAI.MUB6.Certificate.PairSemantics.canonical7626 line 211
  45. def OAI.MUB6.Certificate.PairSemantics.raw7627 line 225
  46. def OAI.MUB6.Certificate.PairSemantics.raw7627step0 line 227
  47. def OAI.MUB6.Certificate.PairSemantics.raw7627step1 line 229
  48. theorem OAI.MUB6.Certificate.PairSemantics.canonical7627 line 231
  49. def OAI.MUB6.Certificate.PairSemantics.raw7628 line 245
  50. def OAI.MUB6.Certificate.PairSemantics.raw7628step0 line 247
  51. def OAI.MUB6.Certificate.PairSemantics.raw7628step1 line 249
  52. def OAI.MUB6.Certificate.PairSemantics.raw7628step2 line 251
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical7628 line 253
  54. def OAI.MUB6.Certificate.PairSemantics.raw7629 line 272
  55. def OAI.MUB6.Certificate.PairSemantics.raw7629step0 line 274
  56. def OAI.MUB6.Certificate.PairSemantics.raw7629step1 line 276
  57. def OAI.MUB6.Certificate.PairSemantics.raw7629step2 line 278
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical7629 line 280
  59. def OAI.MUB6.Certificate.PairSemantics.raw7630 line 299
  60. def OAI.MUB6.Certificate.PairSemantics.raw7630step0 line 301
  61. def OAI.MUB6.Certificate.PairSemantics.raw7630step1 line 303
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical7630 line 305
  63. def OAI.MUB6.Certificate.PairSemantics.raw7631 line 319
  64. def OAI.MUB6.Certificate.PairSemantics.raw7631step0 line 321
  65. def OAI.MUB6.Certificate.PairSemantics.raw7631step1 line 323
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical7631 line 325
  67. def OAI.MUB6.Certificate.PairSemantics.raw7632 line 339
  68. def OAI.MUB6.Certificate.PairSemantics.raw7632step0 line 341
  69. def OAI.MUB6.Certificate.PairSemantics.raw7632step1 line 343
  70. def OAI.MUB6.Certificate.PairSemantics.raw7632step2 line 345
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical7632 line 347
  72. def OAI.MUB6.Certificate.PairSemantics.raw7633 line 366
  73. def OAI.MUB6.Certificate.PairSemantics.raw7633step0 line 368
  74. def OAI.MUB6.Certificate.PairSemantics.raw7633step1 line 370
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical7633 line 372
  76. def OAI.MUB6.Certificate.PairSemantics.raw7634 line 386
  77. def OAI.MUB6.Certificate.PairSemantics.raw7634step0 line 388
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical7634 line 390
  79. def OAI.MUB6.Certificate.PairSemantics.raw7635 line 399
  80. def OAI.MUB6.Certificate.PairSemantics.raw7635step0 line 401
  81. def OAI.MUB6.Certificate.PairSemantics.raw7635step1 line 403
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical7635 line 405
  83. def OAI.MUB6.Certificate.PairSemantics.raw7636 line 419
  84. def OAI.MUB6.Certificate.PairSemantics.raw7636step0 line 421
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical7636 line 423
  86. def OAI.MUB6.Certificate.PairSemantics.raw7637 line 432
  87. def OAI.MUB6.Certificate.PairSemantics.raw7637step0 line 434
  88. def OAI.MUB6.Certificate.PairSemantics.raw7637step1 line 436
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical7637 line 438
  90. def OAI.MUB6.Certificate.PairSemantics.raw7638 line 452
  91. def OAI.MUB6.Certificate.PairSemantics.raw7638step0 line 454
  92. def OAI.MUB6.Certificate.PairSemantics.raw7638step1 line 456
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical7638 line 458
  94. def OAI.MUB6.Certificate.PairSemantics.raw7639 line 472
  95. def OAI.MUB6.Certificate.PairSemantics.raw7639step0 line 474
  96. theorem OAI.MUB6.Certificate.PairSemantics.canonical7639 line 476
  97. def OAI.MUB6.Certificate.PairSemantics.raw7640 line 485
  98. def OAI.MUB6.Certificate.PairSemantics.raw7640step0 line 487
  99. def OAI.MUB6.Certificate.PairSemantics.raw7640step1 line 489
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical7640 line 491
  101. def OAI.MUB6.Certificate.PairSemantics.raw7641 line 505
  102. def OAI.MUB6.Certificate.PairSemantics.raw7641step0 line 507
  103. def OAI.MUB6.Certificate.PairSemantics.raw7641step1 line 509
  104. def OAI.MUB6.Certificate.PairSemantics.raw7641step2 line 511
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical7641 line 513
  106. def OAI.MUB6.Certificate.PairSemantics.raw7642 line 532
  107. def OAI.MUB6.Certificate.PairSemantics.raw7642step0 line 534
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical7642 line 536
  109. def OAI.MUB6.Certificate.PairSemantics.raw7643 line 545
  110. def OAI.MUB6.Certificate.PairSemantics.raw7643step0 line 547
  111. def OAI.MUB6.Certificate.PairSemantics.raw7643step1 line 549
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical7643 line 551
  113. def OAI.MUB6.Certificate.PairSemantics.raw7644 line 565
  114. def OAI.MUB6.Certificate.PairSemantics.raw7644step0 line 567
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical7644 line 569
  116. def OAI.MUB6.Certificate.PairSemantics.raw7645 line 578
  117. def OAI.MUB6.Certificate.PairSemantics.raw7645step0 line 580
  118. theorem OAI.MUB6.Certificate.PairSemantics.canonical7645 line 582
  119. def OAI.MUB6.Certificate.PairSemantics.raw7646 line 591
  120. def OAI.MUB6.Certificate.PairSemantics.raw7646step0 line 593
  121. theorem OAI.MUB6.Certificate.PairSemantics.canonical7646 line 595
  122. def OAI.MUB6.Certificate.PairSemantics.raw7647 line 604
  123. def OAI.MUB6.Certificate.PairSemantics.raw7647step0 line 606
  124. theorem OAI.MUB6.Certificate.PairSemantics.canonical7647 line 608