OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical52.lean

GitHub source file

117 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1664 line 19
  2. def OAI.MUB6.Certificate.PairSemantics.raw1664step0 line 21
  3. def OAI.MUB6.Certificate.PairSemantics.raw1664step1 line 23
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical1664 line 25
  5. def OAI.MUB6.Certificate.PairSemantics.raw1665 line 38
  6. def OAI.MUB6.Certificate.PairSemantics.raw1665step0 line 40
  7. def OAI.MUB6.Certificate.PairSemantics.raw1665step1 line 42
  8. def OAI.MUB6.Certificate.PairSemantics.raw1665step2 line 44
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical1665 line 46
  10. def OAI.MUB6.Certificate.PairSemantics.raw1666 line 63
  11. def OAI.MUB6.Certificate.PairSemantics.raw1666step0 line 65
  12. def OAI.MUB6.Certificate.PairSemantics.raw1666step1 line 67
  13. def OAI.MUB6.Certificate.PairSemantics.raw1666step2 line 69
  14. theorem OAI.MUB6.Certificate.PairSemantics.canonical1666 line 71
  15. def OAI.MUB6.Certificate.PairSemantics.raw1667 line 88
  16. def OAI.MUB6.Certificate.PairSemantics.raw1667step0 line 90
  17. def OAI.MUB6.Certificate.PairSemantics.raw1667step1 line 92
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical1667 line 94
  19. def OAI.MUB6.Certificate.PairSemantics.raw1668 line 107
  20. def OAI.MUB6.Certificate.PairSemantics.raw1668step0 line 109
  21. def OAI.MUB6.Certificate.PairSemantics.raw1668step1 line 111
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical1668 line 113
  23. def OAI.MUB6.Certificate.PairSemantics.raw1669 line 126
  24. def OAI.MUB6.Certificate.PairSemantics.raw1669step0 line 128
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical1669 line 130
  26. def OAI.MUB6.Certificate.PairSemantics.raw1670 line 139
  27. def OAI.MUB6.Certificate.PairSemantics.raw1670step0 line 141
  28. def OAI.MUB6.Certificate.PairSemantics.raw1670step1 line 143
  29. def OAI.MUB6.Certificate.PairSemantics.raw1670step2 line 145
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical1670 line 147
  31. def OAI.MUB6.Certificate.PairSemantics.raw1671 line 165
  32. def OAI.MUB6.Certificate.PairSemantics.raw1671step0 line 167
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical1671 line 169
  34. def OAI.MUB6.Certificate.PairSemantics.raw1672 line 178
  35. def OAI.MUB6.Certificate.PairSemantics.raw1672step0 line 180
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical1672 line 182
  37. def OAI.MUB6.Certificate.PairSemantics.raw1673 line 191
  38. def OAI.MUB6.Certificate.PairSemantics.raw1673step0 line 193
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical1673 line 195
  40. def OAI.MUB6.Certificate.PairSemantics.raw1674 line 204
  41. def OAI.MUB6.Certificate.PairSemantics.raw1674step0 line 206
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical1674 line 208
  43. def OAI.MUB6.Certificate.PairSemantics.raw1675 line 217
  44. def OAI.MUB6.Certificate.PairSemantics.raw1675step0 line 219
  45. def OAI.MUB6.Certificate.PairSemantics.raw1675step1 line 221
  46. def OAI.MUB6.Certificate.PairSemantics.raw1675step2 line 223
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical1675 line 225
  48. def OAI.MUB6.Certificate.PairSemantics.raw1676 line 242
  49. def OAI.MUB6.Certificate.PairSemantics.raw1676step0 line 244
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical1676 line 246
  51. def OAI.MUB6.Certificate.PairSemantics.raw1677 line 255
  52. def OAI.MUB6.Certificate.PairSemantics.raw1677step0 line 257
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical1677 line 259
  54. def OAI.MUB6.Certificate.PairSemantics.raw1678 line 268
  55. def OAI.MUB6.Certificate.PairSemantics.raw1678step0 line 270
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical1678 line 272
  57. def OAI.MUB6.Certificate.PairSemantics.raw1679 line 281
  58. def OAI.MUB6.Certificate.PairSemantics.raw1679step0 line 283
  59. theorem OAI.MUB6.Certificate.PairSemantics.canonical1679 line 285
  60. def OAI.MUB6.Certificate.PairSemantics.raw1680 line 294
  61. def OAI.MUB6.Certificate.PairSemantics.raw1680step0 line 296
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical1680 line 298
  63. def OAI.MUB6.Certificate.PairSemantics.raw1681 line 307
  64. def OAI.MUB6.Certificate.PairSemantics.raw1681step0 line 309
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical1681 line 311
  66. def OAI.MUB6.Certificate.PairSemantics.raw1682 line 320
  67. def OAI.MUB6.Certificate.PairSemantics.raw1682step0 line 322
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical1682 line 324
  69. def OAI.MUB6.Certificate.PairSemantics.raw1683 line 333
  70. def OAI.MUB6.Certificate.PairSemantics.raw1683step0 line 335
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical1683 line 337
  72. def OAI.MUB6.Certificate.PairSemantics.raw1684 line 346
  73. def OAI.MUB6.Certificate.PairSemantics.raw1684step0 line 348
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical1684 line 350
  75. def OAI.MUB6.Certificate.PairSemantics.raw1685 line 359
  76. def OAI.MUB6.Certificate.PairSemantics.raw1685step0 line 361
  77. def OAI.MUB6.Certificate.PairSemantics.raw1685step1 line 363
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical1685 line 365
  79. def OAI.MUB6.Certificate.PairSemantics.raw1686 line 378
  80. def OAI.MUB6.Certificate.PairSemantics.raw1686step0 line 380
  81. def OAI.MUB6.Certificate.PairSemantics.raw1686step1 line 382
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical1686 line 384
  83. def OAI.MUB6.Certificate.PairSemantics.raw1687 line 397
  84. def OAI.MUB6.Certificate.PairSemantics.raw1687step0 line 399
  85. def OAI.MUB6.Certificate.PairSemantics.raw1687step1 line 401
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical1687 line 403
  87. def OAI.MUB6.Certificate.PairSemantics.raw1688 line 416
  88. def OAI.MUB6.Certificate.PairSemantics.raw1688step0 line 418
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical1688 line 420
  90. def OAI.MUB6.Certificate.PairSemantics.raw1689 line 429
  91. def OAI.MUB6.Certificate.PairSemantics.raw1689step0 line 431
  92. def OAI.MUB6.Certificate.PairSemantics.raw1689step1 line 433
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical1689 line 435
  94. def OAI.MUB6.Certificate.PairSemantics.raw1690 line 448
  95. def OAI.MUB6.Certificate.PairSemantics.raw1690step0 line 450
  96. def OAI.MUB6.Certificate.PairSemantics.raw1690step1 line 452
  97. def OAI.MUB6.Certificate.PairSemantics.raw1690step2 line 454
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical1690 line 456
  99. def OAI.MUB6.Certificate.PairSemantics.raw1691 line 473
  100. def OAI.MUB6.Certificate.PairSemantics.raw1691step0 line 475
  101. def OAI.MUB6.Certificate.PairSemantics.raw1691step1 line 477
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical1691 line 479
  103. def OAI.MUB6.Certificate.PairSemantics.raw1692 line 492
  104. def OAI.MUB6.Certificate.PairSemantics.raw1692step0 line 494
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical1692 line 496
  106. def OAI.MUB6.Certificate.PairSemantics.raw1693 line 505
  107. def OAI.MUB6.Certificate.PairSemantics.raw1693step0 line 507
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical1693 line 509
  109. def OAI.MUB6.Certificate.PairSemantics.raw1694 line 518
  110. def OAI.MUB6.Certificate.PairSemantics.raw1694step0 line 520
  111. def OAI.MUB6.Certificate.PairSemantics.raw1694step1 line 522
  112. theorem OAI.MUB6.Certificate.PairSemantics.canonical1694 line 524
  113. def OAI.MUB6.Certificate.PairSemantics.raw1695 line 537
  114. def OAI.MUB6.Certificate.PairSemantics.raw1695step0 line 539
  115. def OAI.MUB6.Certificate.PairSemantics.raw1695step1 line 541
  116. def OAI.MUB6.Certificate.PairSemantics.raw1695step2 line 543
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical1695 line 545