OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical53.lean

GitHub source file

115 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1696 line 16
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical1696 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw1697 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw1697step0 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw1697step1 line 26
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical1697 line 28
  7. def OAI.MUB6.Certificate.PairSemantics.raw1698 line 41
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical1698 line 43
  9. def OAI.MUB6.Certificate.PairSemantics.raw1699 line 47
  10. def OAI.MUB6.Certificate.PairSemantics.raw1699step0 line 49
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical1699 line 51
  12. def OAI.MUB6.Certificate.PairSemantics.raw1700 line 60
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical1700 line 62
  14. def OAI.MUB6.Certificate.PairSemantics.raw1701 line 66
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical1701 line 68
  16. def OAI.MUB6.Certificate.PairSemantics.raw1702 line 72
  17. def OAI.MUB6.Certificate.PairSemantics.raw1702step0 line 74
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical1702 line 76
  19. def OAI.MUB6.Certificate.PairSemantics.raw1703 line 85
  20. def OAI.MUB6.Certificate.PairSemantics.raw1703step0 line 87
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical1703 line 89
  22. def OAI.MUB6.Certificate.PairSemantics.raw1704 line 98
  23. theorem OAI.MUB6.Certificate.PairSemantics.canonical1704 line 100
  24. def OAI.MUB6.Certificate.PairSemantics.raw1705 line 104
  25. def OAI.MUB6.Certificate.PairSemantics.raw1705step0 line 106
  26. def OAI.MUB6.Certificate.PairSemantics.raw1705step1 line 108
  27. def OAI.MUB6.Certificate.PairSemantics.raw1705step2 line 110
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical1705 line 112
  29. def OAI.MUB6.Certificate.PairSemantics.raw1706 line 129
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical1706 line 131
  31. def OAI.MUB6.Certificate.PairSemantics.raw1707 line 135
  32. def OAI.MUB6.Certificate.PairSemantics.raw1707step0 line 137
  33. def OAI.MUB6.Certificate.PairSemantics.raw1707step1 line 139
  34. def OAI.MUB6.Certificate.PairSemantics.raw1707step2 line 141
  35. theorem OAI.MUB6.Certificate.PairSemantics.canonical1707 line 143
  36. def OAI.MUB6.Certificate.PairSemantics.raw1708 line 160
  37. def OAI.MUB6.Certificate.PairSemantics.raw1708step0 line 162
  38. def OAI.MUB6.Certificate.PairSemantics.raw1708step1 line 164
  39. def OAI.MUB6.Certificate.PairSemantics.raw1708step2 line 166
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical1708 line 168
  41. def OAI.MUB6.Certificate.PairSemantics.raw1709 line 185
  42. def OAI.MUB6.Certificate.PairSemantics.raw1709step0 line 187
  43. def OAI.MUB6.Certificate.PairSemantics.raw1709step1 line 189
  44. def OAI.MUB6.Certificate.PairSemantics.raw1709step2 line 191
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical1709 line 193
  46. def OAI.MUB6.Certificate.PairSemantics.raw1710 line 210
  47. def OAI.MUB6.Certificate.PairSemantics.raw1710step0 line 212
  48. def OAI.MUB6.Certificate.PairSemantics.raw1710step1 line 214
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical1710 line 216
  50. def OAI.MUB6.Certificate.PairSemantics.raw1711 line 229
  51. def OAI.MUB6.Certificate.PairSemantics.raw1711step0 line 231
  52. def OAI.MUB6.Certificate.PairSemantics.raw1711step1 line 233
  53. def OAI.MUB6.Certificate.PairSemantics.raw1711step2 line 235
  54. theorem OAI.MUB6.Certificate.PairSemantics.canonical1711 line 237
  55. def OAI.MUB6.Certificate.PairSemantics.raw1712 line 254
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical1712 line 256
  57. def OAI.MUB6.Certificate.PairSemantics.raw1713 line 260
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical1713 line 262
  59. def OAI.MUB6.Certificate.PairSemantics.raw1714 line 266
  60. def OAI.MUB6.Certificate.PairSemantics.raw1714step0 line 268
  61. def OAI.MUB6.Certificate.PairSemantics.raw1714step1 line 270
  62. theorem OAI.MUB6.Certificate.PairSemantics.canonical1714 line 272
  63. def OAI.MUB6.Certificate.PairSemantics.raw1715 line 285
  64. def OAI.MUB6.Certificate.PairSemantics.raw1715step0 line 287
  65. def OAI.MUB6.Certificate.PairSemantics.raw1715step1 line 289
  66. def OAI.MUB6.Certificate.PairSemantics.raw1715step2 line 291
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical1715 line 293
  68. def OAI.MUB6.Certificate.PairSemantics.raw1716 line 310
  69. def OAI.MUB6.Certificate.PairSemantics.raw1716step0 line 312
  70. theorem OAI.MUB6.Certificate.PairSemantics.canonical1716 line 314
  71. def OAI.MUB6.Certificate.PairSemantics.raw1717 line 323
  72. def OAI.MUB6.Certificate.PairSemantics.raw1717step0 line 325
  73. def OAI.MUB6.Certificate.PairSemantics.raw1717step1 line 327
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical1717 line 329
  75. def OAI.MUB6.Certificate.PairSemantics.raw1718 line 342
  76. def OAI.MUB6.Certificate.PairSemantics.raw1718step0 line 344
  77. def OAI.MUB6.Certificate.PairSemantics.raw1718step1 line 346
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical1718 line 348
  79. def OAI.MUB6.Certificate.PairSemantics.raw1719 line 361
  80. def OAI.MUB6.Certificate.PairSemantics.raw1719step0 line 363
  81. def OAI.MUB6.Certificate.PairSemantics.raw1719step1 line 365
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical1719 line 367
  83. def OAI.MUB6.Certificate.PairSemantics.raw1720 line 380
  84. def OAI.MUB6.Certificate.PairSemantics.raw1720step0 line 382
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical1720 line 384
  86. def OAI.MUB6.Certificate.PairSemantics.raw1721 line 393
  87. def OAI.MUB6.Certificate.PairSemantics.raw1721step0 line 395
  88. theorem OAI.MUB6.Certificate.PairSemantics.canonical1721 line 397
  89. def OAI.MUB6.Certificate.PairSemantics.raw1722 line 406
  90. def OAI.MUB6.Certificate.PairSemantics.raw1722step0 line 408
  91. def OAI.MUB6.Certificate.PairSemantics.raw1722step1 line 410
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical1722 line 412
  93. def OAI.MUB6.Certificate.PairSemantics.raw1723 line 425
  94. def OAI.MUB6.Certificate.PairSemantics.raw1723step0 line 427
  95. def OAI.MUB6.Certificate.PairSemantics.raw1723step1 line 429
  96. def OAI.MUB6.Certificate.PairSemantics.raw1723step2 line 431
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical1723 line 433
  98. def OAI.MUB6.Certificate.PairSemantics.raw1724 line 450
  99. def OAI.MUB6.Certificate.PairSemantics.raw1724step0 line 452
  100. def OAI.MUB6.Certificate.PairSemantics.raw1724step1 line 454
  101. def OAI.MUB6.Certificate.PairSemantics.raw1724step2 line 456
  102. theorem OAI.MUB6.Certificate.PairSemantics.canonical1724 line 458
  103. def OAI.MUB6.Certificate.PairSemantics.raw1725 line 475
  104. def OAI.MUB6.Certificate.PairSemantics.raw1725step0 line 477
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical1725 line 479
  106. def OAI.MUB6.Certificate.PairSemantics.raw1726 line 488
  107. def OAI.MUB6.Certificate.PairSemantics.raw1726step0 line 490
  108. def OAI.MUB6.Certificate.PairSemantics.raw1726step1 line 492
  109. def OAI.MUB6.Certificate.PairSemantics.raw1726step2 line 494
  110. theorem OAI.MUB6.Certificate.PairSemantics.canonical1726 line 496
  111. def OAI.MUB6.Certificate.PairSemantics.raw1727 line 513
  112. def OAI.MUB6.Certificate.PairSemantics.raw1727step0 line 515
  113. def OAI.MUB6.Certificate.PairSemantics.raw1727step1 line 517
  114. def OAI.MUB6.Certificate.PairSemantics.raw1727step2 line 519
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical1727 line 521