OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical51.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1632 line 18
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical1632 line 20
  3. def OAI.MUB6.Certificate.PairSemantics.raw1633 line 24
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical1633 line 26
  5. def OAI.MUB6.Certificate.PairSemantics.raw1634 line 30
  6. def OAI.MUB6.Certificate.PairSemantics.raw1634step0 line 32
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical1634 line 34
  8. def OAI.MUB6.Certificate.PairSemantics.raw1635 line 43
  9. theorem OAI.MUB6.Certificate.PairSemantics.canonical1635 line 45
  10. def OAI.MUB6.Certificate.PairSemantics.raw1636 line 49
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical1636 line 51
  12. def OAI.MUB6.Certificate.PairSemantics.raw1637 line 55
  13. def OAI.MUB6.Certificate.PairSemantics.raw1637step0 line 57
  14. def OAI.MUB6.Certificate.PairSemantics.raw1637step1 line 59
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical1637 line 61
  16. def OAI.MUB6.Certificate.PairSemantics.raw1638 line 74
  17. theorem OAI.MUB6.Certificate.PairSemantics.canonical1638 line 76
  18. def OAI.MUB6.Certificate.PairSemantics.raw1639 line 80
  19. def OAI.MUB6.Certificate.PairSemantics.raw1639step0 line 82
  20. def OAI.MUB6.Certificate.PairSemantics.raw1639step1 line 84
  21. def OAI.MUB6.Certificate.PairSemantics.raw1639step2 line 86
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical1639 line 88
  23. def OAI.MUB6.Certificate.PairSemantics.raw1640 line 105
  24. def OAI.MUB6.Certificate.PairSemantics.raw1640step0 line 107
  25. def OAI.MUB6.Certificate.PairSemantics.raw1640step1 line 109
  26. theorem OAI.MUB6.Certificate.PairSemantics.canonical1640 line 111
  27. def OAI.MUB6.Certificate.PairSemantics.raw1641 line 124
  28. def OAI.MUB6.Certificate.PairSemantics.raw1641step0 line 126
  29. theorem OAI.MUB6.Certificate.PairSemantics.canonical1641 line 128
  30. def OAI.MUB6.Certificate.PairSemantics.raw1642 line 137
  31. def OAI.MUB6.Certificate.PairSemantics.raw1642step0 line 139
  32. def OAI.MUB6.Certificate.PairSemantics.raw1642step1 line 141
  33. theorem OAI.MUB6.Certificate.PairSemantics.canonical1642 line 143
  34. def OAI.MUB6.Certificate.PairSemantics.raw1643 line 156
  35. def OAI.MUB6.Certificate.PairSemantics.raw1643step0 line 158
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical1643 line 160
  37. def OAI.MUB6.Certificate.PairSemantics.raw1644 line 169
  38. def OAI.MUB6.Certificate.PairSemantics.raw1644step0 line 171
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical1644 line 173
  40. def OAI.MUB6.Certificate.PairSemantics.raw1645 line 182
  41. def OAI.MUB6.Certificate.PairSemantics.raw1645step0 line 184
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical1645 line 186
  43. def OAI.MUB6.Certificate.PairSemantics.raw1646 line 195
  44. def OAI.MUB6.Certificate.PairSemantics.raw1646step0 line 197
  45. def OAI.MUB6.Certificate.PairSemantics.raw1646step1 line 199
  46. theorem OAI.MUB6.Certificate.PairSemantics.canonical1646 line 201
  47. def OAI.MUB6.Certificate.PairSemantics.raw1647 line 214
  48. def OAI.MUB6.Certificate.PairSemantics.raw1647step0 line 216
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical1647 line 218
  50. def OAI.MUB6.Certificate.PairSemantics.raw1648 line 227
  51. theorem OAI.MUB6.Certificate.PairSemantics.canonical1648 line 229
  52. def OAI.MUB6.Certificate.PairSemantics.raw1649 line 233
  53. def OAI.MUB6.Certificate.PairSemantics.raw1649step0 line 235
  54. def OAI.MUB6.Certificate.PairSemantics.raw1649step1 line 237
  55. def OAI.MUB6.Certificate.PairSemantics.raw1649step2 line 239
  56. theorem OAI.MUB6.Certificate.PairSemantics.canonical1649 line 241
  57. def OAI.MUB6.Certificate.PairSemantics.raw1650 line 258
  58. def OAI.MUB6.Certificate.PairSemantics.raw1650step0 line 260
  59. def OAI.MUB6.Certificate.PairSemantics.raw1650step1 line 262
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical1650 line 264
  61. def OAI.MUB6.Certificate.PairSemantics.raw1651 line 277
  62. def OAI.MUB6.Certificate.PairSemantics.raw1651step0 line 279
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical1651 line 281
  64. def OAI.MUB6.Certificate.PairSemantics.raw1652 line 290
  65. theorem OAI.MUB6.Certificate.PairSemantics.canonical1652 line 292
  66. def OAI.MUB6.Certificate.PairSemantics.raw1653 line 296
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical1653 line 298
  68. def OAI.MUB6.Certificate.PairSemantics.raw1654 line 302
  69. def OAI.MUB6.Certificate.PairSemantics.raw1654step0 line 304
  70. def OAI.MUB6.Certificate.PairSemantics.raw1654step1 line 306
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical1654 line 308
  72. def OAI.MUB6.Certificate.PairSemantics.raw1655 line 321
  73. def OAI.MUB6.Certificate.PairSemantics.raw1655step0 line 323
  74. theorem OAI.MUB6.Certificate.PairSemantics.canonical1655 line 325
  75. def OAI.MUB6.Certificate.PairSemantics.raw1656 line 334
  76. def OAI.MUB6.Certificate.PairSemantics.raw1656step0 line 336
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical1656 line 338
  78. def OAI.MUB6.Certificate.PairSemantics.raw1657 line 347
  79. def OAI.MUB6.Certificate.PairSemantics.raw1657step0 line 349
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical1657 line 351
  81. def OAI.MUB6.Certificate.PairSemantics.raw1658 line 360
  82. def OAI.MUB6.Certificate.PairSemantics.raw1658step0 line 362
  83. def OAI.MUB6.Certificate.PairSemantics.raw1658step1 line 364
  84. def OAI.MUB6.Certificate.PairSemantics.raw1658step2 line 366
  85. theorem OAI.MUB6.Certificate.PairSemantics.canonical1658 line 368
  86. def OAI.MUB6.Certificate.PairSemantics.raw1659 line 385
  87. def OAI.MUB6.Certificate.PairSemantics.raw1659step0 line 387
  88. def OAI.MUB6.Certificate.PairSemantics.raw1659step1 line 389
  89. def OAI.MUB6.Certificate.PairSemantics.raw1659step2 line 391
  90. theorem OAI.MUB6.Certificate.PairSemantics.canonical1659 line 393
  91. def OAI.MUB6.Certificate.PairSemantics.raw1660 line 410
  92. def OAI.MUB6.Certificate.PairSemantics.raw1660step0 line 412
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical1660 line 414
  94. def OAI.MUB6.Certificate.PairSemantics.raw1661 line 423
  95. theorem OAI.MUB6.Certificate.PairSemantics.canonical1661 line 425
  96. def OAI.MUB6.Certificate.PairSemantics.raw1662 line 429
  97. def OAI.MUB6.Certificate.PairSemantics.raw1662step0 line 431
  98. def OAI.MUB6.Certificate.PairSemantics.raw1662step1 line 433
  99. theorem OAI.MUB6.Certificate.PairSemantics.canonical1662 line 435
  100. def OAI.MUB6.Certificate.PairSemantics.raw1663 line 448
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical1663 line 450