OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical54.lean

GitHub source file

113 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1728 line 21
  2. def OAI.MUB6.Certificate.PairSemantics.raw1728step0 line 23
  3. def OAI.MUB6.Certificate.PairSemantics.raw1728step1 line 25
  4. def OAI.MUB6.Certificate.PairSemantics.raw1728step2 line 27
  5. theorem OAI.MUB6.Certificate.PairSemantics.canonical1728 line 29
  6. def OAI.MUB6.Certificate.PairSemantics.raw1729 line 46
  7. def OAI.MUB6.Certificate.PairSemantics.raw1729step0 line 48
  8. def OAI.MUB6.Certificate.PairSemantics.raw1729step1 line 50
  9. def OAI.MUB6.Certificate.PairSemantics.raw1729step2 line 52
  10. theorem OAI.MUB6.Certificate.PairSemantics.canonical1729 line 54
  11. def OAI.MUB6.Certificate.PairSemantics.raw1730 line 71
  12. def OAI.MUB6.Certificate.PairSemantics.raw1730step0 line 73
  13. def OAI.MUB6.Certificate.PairSemantics.raw1730step1 line 75
  14. def OAI.MUB6.Certificate.PairSemantics.raw1730step2 line 77
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical1730 line 79
  16. def OAI.MUB6.Certificate.PairSemantics.raw1731 line 96
  17. def OAI.MUB6.Certificate.PairSemantics.raw1731step0 line 98
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical1731 line 100
  19. def OAI.MUB6.Certificate.PairSemantics.raw1732 line 109
  20. def OAI.MUB6.Certificate.PairSemantics.raw1732step0 line 111
  21. def OAI.MUB6.Certificate.PairSemantics.raw1732step1 line 113
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical1732 line 115
  23. def OAI.MUB6.Certificate.PairSemantics.raw1733 line 128
  24. def OAI.MUB6.Certificate.PairSemantics.raw1733step0 line 130
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical1733 line 132
  26. def OAI.MUB6.Certificate.PairSemantics.raw1734 line 141
  27. def OAI.MUB6.Certificate.PairSemantics.raw1734step0 line 143
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical1734 line 145
  29. def OAI.MUB6.Certificate.PairSemantics.raw1735 line 154
  30. def OAI.MUB6.Certificate.PairSemantics.raw1735step0 line 156
  31. def OAI.MUB6.Certificate.PairSemantics.raw1735step1 line 158
  32. theorem OAI.MUB6.Certificate.PairSemantics.canonical1735 line 160
  33. def OAI.MUB6.Certificate.PairSemantics.raw1736 line 173
  34. def OAI.MUB6.Certificate.PairSemantics.raw1736step0 line 175
  35. def OAI.MUB6.Certificate.PairSemantics.raw1736step1 line 177
  36. def OAI.MUB6.Certificate.PairSemantics.raw1736step2 line 179
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical1736 line 181
  38. def OAI.MUB6.Certificate.PairSemantics.raw1737 line 198
  39. def OAI.MUB6.Certificate.PairSemantics.raw1737step0 line 200
  40. theorem OAI.MUB6.Certificate.PairSemantics.canonical1737 line 202
  41. def OAI.MUB6.Certificate.PairSemantics.raw1738 line 211
  42. def OAI.MUB6.Certificate.PairSemantics.raw1738step0 line 213
  43. theorem OAI.MUB6.Certificate.PairSemantics.canonical1738 line 215
  44. def OAI.MUB6.Certificate.PairSemantics.raw1739 line 224
  45. def OAI.MUB6.Certificate.PairSemantics.raw1739step0 line 226
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical1739 line 228
  47. def OAI.MUB6.Certificate.PairSemantics.raw1740 line 237
  48. def OAI.MUB6.Certificate.PairSemantics.raw1740step0 line 239
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical1740 line 241
  50. def OAI.MUB6.Certificate.PairSemantics.raw1741 line 250
  51. def OAI.MUB6.Certificate.PairSemantics.raw1741step0 line 252
  52. def OAI.MUB6.Certificate.PairSemantics.raw1741step1 line 254
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical1741 line 256
  54. def OAI.MUB6.Certificate.PairSemantics.raw1742 line 269
  55. def OAI.MUB6.Certificate.PairSemantics.raw1742step0 line 271
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical1742 line 273
  57. def OAI.MUB6.Certificate.PairSemantics.raw1743 line 282
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical1743 line 284
  59. def OAI.MUB6.Certificate.PairSemantics.raw1744 line 288
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical1744 line 290
  61. def OAI.MUB6.Certificate.PairSemantics.raw1745 line 294
  62. def OAI.MUB6.Certificate.PairSemantics.raw1745step0 line 296
  63. def OAI.MUB6.Certificate.PairSemantics.raw1745step1 line 298
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical1745 line 300
  65. def OAI.MUB6.Certificate.PairSemantics.raw1746 line 313
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical1746 line 315
  67. def OAI.MUB6.Certificate.PairSemantics.raw1747 line 319
  68. def OAI.MUB6.Certificate.PairSemantics.raw1747step0 line 321
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical1747 line 323
  70. def OAI.MUB6.Certificate.PairSemantics.raw1748 line 332
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical1748 line 334
  72. def OAI.MUB6.Certificate.PairSemantics.raw1749 line 338
  73. theorem OAI.MUB6.Certificate.PairSemantics.canonical1749 line 340
  74. def OAI.MUB6.Certificate.PairSemantics.raw1750 line 344
  75. def OAI.MUB6.Certificate.PairSemantics.raw1750step0 line 346
  76. def OAI.MUB6.Certificate.PairSemantics.raw1750step1 line 348
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical1750 line 350
  78. def OAI.MUB6.Certificate.PairSemantics.raw1751 line 363
  79. def OAI.MUB6.Certificate.PairSemantics.raw1751step0 line 365
  80. def OAI.MUB6.Certificate.PairSemantics.raw1751step1 line 367
  81. theorem OAI.MUB6.Certificate.PairSemantics.canonical1751 line 369
  82. def OAI.MUB6.Certificate.PairSemantics.raw1752 line 382
  83. def OAI.MUB6.Certificate.PairSemantics.raw1752step0 line 384
  84. def OAI.MUB6.Certificate.PairSemantics.raw1752step1 line 386
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical1752 line 388
  86. def OAI.MUB6.Certificate.PairSemantics.raw1753 line 401
  87. def OAI.MUB6.Certificate.PairSemantics.raw1753step0 line 403
  88. def OAI.MUB6.Certificate.PairSemantics.raw1753step1 line 405
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical1753 line 407
  90. def OAI.MUB6.Certificate.PairSemantics.raw1754 line 420
  91. def OAI.MUB6.Certificate.PairSemantics.raw1754step0 line 422
  92. def OAI.MUB6.Certificate.PairSemantics.raw1754step1 line 424
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical1754 line 426
  94. def OAI.MUB6.Certificate.PairSemantics.raw1755 line 439
  95. def OAI.MUB6.Certificate.PairSemantics.raw1755step0 line 441
  96. def OAI.MUB6.Certificate.PairSemantics.raw1755step1 line 443
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical1755 line 445
  98. def OAI.MUB6.Certificate.PairSemantics.raw1756 line 458
  99. def OAI.MUB6.Certificate.PairSemantics.raw1756step0 line 460
  100. def OAI.MUB6.Certificate.PairSemantics.raw1756step1 line 462
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical1756 line 464
  102. def OAI.MUB6.Certificate.PairSemantics.raw1757 line 477
  103. def OAI.MUB6.Certificate.PairSemantics.raw1757step0 line 479
  104. def OAI.MUB6.Certificate.PairSemantics.raw1757step1 line 481
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical1757 line 483
  106. def OAI.MUB6.Certificate.PairSemantics.raw1758 line 496
  107. def OAI.MUB6.Certificate.PairSemantics.raw1758step0 line 498
  108. def OAI.MUB6.Certificate.PairSemantics.raw1758step1 line 500
  109. theorem OAI.MUB6.Certificate.PairSemantics.canonical1758 line 502
  110. def OAI.MUB6.Certificate.PairSemantics.raw1759 line 515
  111. def OAI.MUB6.Certificate.PairSemantics.raw1759step0 line 517
  112. def OAI.MUB6.Certificate.PairSemantics.raw1759step1 line 519
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical1759 line 521