OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical56.lean

GitHub source file

98 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1792 line 16
  2. theorem OAI.MUB6.Certificate.PairSemantics.canonical1792 line 18
  3. def OAI.MUB6.Certificate.PairSemantics.raw1793 line 22
  4. def OAI.MUB6.Certificate.PairSemantics.raw1793step0 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw1793step1 line 26
  6. def OAI.MUB6.Certificate.PairSemantics.raw1793step2 line 28
  7. theorem OAI.MUB6.Certificate.PairSemantics.canonical1793 line 30
  8. def OAI.MUB6.Certificate.PairSemantics.raw1794 line 47
  9. def OAI.MUB6.Certificate.PairSemantics.raw1794step0 line 49
  10. def OAI.MUB6.Certificate.PairSemantics.raw1794step1 line 51
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical1794 line 53
  12. def OAI.MUB6.Certificate.PairSemantics.raw1795 line 66
  13. theorem OAI.MUB6.Certificate.PairSemantics.canonical1795 line 68
  14. def OAI.MUB6.Certificate.PairSemantics.raw1796 line 72
  15. theorem OAI.MUB6.Certificate.PairSemantics.canonical1796 line 74
  16. def OAI.MUB6.Certificate.PairSemantics.raw1797 line 78
  17. def OAI.MUB6.Certificate.PairSemantics.raw1797step0 line 80
  18. theorem OAI.MUB6.Certificate.PairSemantics.canonical1797 line 82
  19. def OAI.MUB6.Certificate.PairSemantics.raw1798 line 91
  20. def OAI.MUB6.Certificate.PairSemantics.raw1798step0 line 93
  21. def OAI.MUB6.Certificate.PairSemantics.raw1798step1 line 95
  22. theorem OAI.MUB6.Certificate.PairSemantics.canonical1798 line 97
  23. def OAI.MUB6.Certificate.PairSemantics.raw1799 line 110
  24. def OAI.MUB6.Certificate.PairSemantics.raw1799step0 line 112
  25. def OAI.MUB6.Certificate.PairSemantics.raw1799step1 line 114
  26. def OAI.MUB6.Certificate.PairSemantics.raw1799step2 line 116
  27. theorem OAI.MUB6.Certificate.PairSemantics.canonical1799 line 118
  28. def OAI.MUB6.Certificate.PairSemantics.raw1800 line 135
  29. def OAI.MUB6.Certificate.PairSemantics.raw1800step0 line 137
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical1800 line 139
  31. def OAI.MUB6.Certificate.PairSemantics.raw1801 line 148
  32. def OAI.MUB6.Certificate.PairSemantics.raw1801step0 line 150
  33. def OAI.MUB6.Certificate.PairSemantics.raw1801step1 line 152
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical1801 line 154
  35. def OAI.MUB6.Certificate.PairSemantics.raw1802 line 167
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical1802 line 169
  37. def OAI.MUB6.Certificate.PairSemantics.raw1803 line 173
  38. theorem OAI.MUB6.Certificate.PairSemantics.canonical1803 line 175
  39. def OAI.MUB6.Certificate.PairSemantics.raw1804 line 179
  40. def OAI.MUB6.Certificate.PairSemantics.raw1804step0 line 181
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical1804 line 183
  42. def OAI.MUB6.Certificate.PairSemantics.raw1805 line 192
  43. def OAI.MUB6.Certificate.PairSemantics.raw1805step0 line 194
  44. def OAI.MUB6.Certificate.PairSemantics.raw1805step1 line 196
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical1805 line 198
  46. def OAI.MUB6.Certificate.PairSemantics.raw1806 line 211
  47. theorem OAI.MUB6.Certificate.PairSemantics.canonical1806 line 213
  48. def OAI.MUB6.Certificate.PairSemantics.raw1807 line 217
  49. theorem OAI.MUB6.Certificate.PairSemantics.canonical1807 line 219
  50. def OAI.MUB6.Certificate.PairSemantics.raw1808 line 223
  51. def OAI.MUB6.Certificate.PairSemantics.raw1808step0 line 225
  52. theorem OAI.MUB6.Certificate.PairSemantics.canonical1808 line 227
  53. def OAI.MUB6.Certificate.PairSemantics.raw1809 line 236
  54. def OAI.MUB6.Certificate.PairSemantics.raw1809step0 line 238
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical1809 line 240
  56. def OAI.MUB6.Certificate.PairSemantics.raw1810 line 249
  57. def OAI.MUB6.Certificate.PairSemantics.raw1810step0 line 251
  58. theorem OAI.MUB6.Certificate.PairSemantics.canonical1810 line 253
  59. def OAI.MUB6.Certificate.PairSemantics.raw1811 line 262
  60. def OAI.MUB6.Certificate.PairSemantics.raw1811step0 line 264
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical1811 line 266
  62. def OAI.MUB6.Certificate.PairSemantics.raw1812 line 275
  63. theorem OAI.MUB6.Certificate.PairSemantics.canonical1812 line 277
  64. def OAI.MUB6.Certificate.PairSemantics.raw1813 line 281
  65. def OAI.MUB6.Certificate.PairSemantics.raw1813step0 line 283
  66. def OAI.MUB6.Certificate.PairSemantics.raw1813step1 line 285
  67. theorem OAI.MUB6.Certificate.PairSemantics.canonical1813 line 287
  68. def OAI.MUB6.Certificate.PairSemantics.raw1814 line 300
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical1814 line 302
  70. def OAI.MUB6.Certificate.PairSemantics.raw1815 line 306
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical1815 line 308
  72. def OAI.MUB6.Certificate.PairSemantics.raw1816 line 312
  73. def OAI.MUB6.Certificate.PairSemantics.raw1816step0 line 314
  74. def OAI.MUB6.Certificate.PairSemantics.raw1816step1 line 316
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical1816 line 318
  76. def OAI.MUB6.Certificate.PairSemantics.raw1817 line 331
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical1817 line 333
  78. def OAI.MUB6.Certificate.PairSemantics.raw1818 line 337
  79. def OAI.MUB6.Certificate.PairSemantics.raw1818step0 line 339
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical1818 line 341
  81. def OAI.MUB6.Certificate.PairSemantics.raw1819 line 350
  82. def OAI.MUB6.Certificate.PairSemantics.raw1819step0 line 352
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical1819 line 354
  84. def OAI.MUB6.Certificate.PairSemantics.raw1820 line 363
  85. def OAI.MUB6.Certificate.PairSemantics.raw1820step0 line 365
  86. def OAI.MUB6.Certificate.PairSemantics.raw1820step1 line 367
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical1820 line 369
  88. def OAI.MUB6.Certificate.PairSemantics.raw1821 line 382
  89. def OAI.MUB6.Certificate.PairSemantics.raw1821step0 line 384
  90. def OAI.MUB6.Certificate.PairSemantics.raw1821step1 line 386
  91. theorem OAI.MUB6.Certificate.PairSemantics.canonical1821 line 388
  92. def OAI.MUB6.Certificate.PairSemantics.raw1822 line 401
  93. def OAI.MUB6.Certificate.PairSemantics.raw1822step0 line 403
  94. theorem OAI.MUB6.Certificate.PairSemantics.canonical1822 line 405
  95. def OAI.MUB6.Certificate.PairSemantics.raw1823 line 414
  96. def OAI.MUB6.Certificate.PairSemantics.raw1823step0 line 416
  97. def OAI.MUB6.Certificate.PairSemantics.raw1823step1 line 418
  98. theorem OAI.MUB6.Certificate.PairSemantics.canonical1823 line 420