OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical57.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1824 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw1824step0 line 20
  3. def OAI.MUB6.Certificate.PairSemantics.raw1824step1 line 22
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical1824 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw1825 line 37
  6. theorem OAI.MUB6.Certificate.PairSemantics.canonical1825 line 39
  7. def OAI.MUB6.Certificate.PairSemantics.raw1826 line 43
  8. def OAI.MUB6.Certificate.PairSemantics.raw1826step0 line 45
  9. def OAI.MUB6.Certificate.PairSemantics.raw1826step1 line 47
  10. def OAI.MUB6.Certificate.PairSemantics.raw1826step2 line 49
  11. theorem OAI.MUB6.Certificate.PairSemantics.canonical1826 line 51
  12. def OAI.MUB6.Certificate.PairSemantics.raw1827 line 69
  13. def OAI.MUB6.Certificate.PairSemantics.raw1827step0 line 71
  14. def OAI.MUB6.Certificate.PairSemantics.raw1827step1 line 73
  15. def OAI.MUB6.Certificate.PairSemantics.raw1827step2 line 75
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical1827 line 77
  17. def OAI.MUB6.Certificate.PairSemantics.raw1828 line 95
  18. def OAI.MUB6.Certificate.PairSemantics.raw1828step0 line 97
  19. def OAI.MUB6.Certificate.PairSemantics.raw1828step1 line 99
  20. def OAI.MUB6.Certificate.PairSemantics.raw1828step2 line 101
  21. theorem OAI.MUB6.Certificate.PairSemantics.canonical1828 line 103
  22. def OAI.MUB6.Certificate.PairSemantics.raw1829 line 121
  23. def OAI.MUB6.Certificate.PairSemantics.raw1829step0 line 123
  24. def OAI.MUB6.Certificate.PairSemantics.raw1829step1 line 125
  25. theorem OAI.MUB6.Certificate.PairSemantics.canonical1829 line 127
  26. def OAI.MUB6.Certificate.PairSemantics.raw1830 line 141
  27. def OAI.MUB6.Certificate.PairSemantics.raw1830step0 line 143
  28. theorem OAI.MUB6.Certificate.PairSemantics.canonical1830 line 145
  29. def OAI.MUB6.Certificate.PairSemantics.raw1831 line 154
  30. def OAI.MUB6.Certificate.PairSemantics.raw1831step0 line 156
  31. theorem OAI.MUB6.Certificate.PairSemantics.canonical1831 line 158
  32. def OAI.MUB6.Certificate.PairSemantics.raw1832 line 167
  33. def OAI.MUB6.Certificate.PairSemantics.raw1832step0 line 169
  34. theorem OAI.MUB6.Certificate.PairSemantics.canonical1832 line 171
  35. def OAI.MUB6.Certificate.PairSemantics.raw1833 line 180
  36. def OAI.MUB6.Certificate.PairSemantics.raw1833step0 line 182
  37. theorem OAI.MUB6.Certificate.PairSemantics.canonical1833 line 184
  38. def OAI.MUB6.Certificate.PairSemantics.raw1834 line 193
  39. theorem OAI.MUB6.Certificate.PairSemantics.canonical1834 line 195
  40. def OAI.MUB6.Certificate.PairSemantics.raw1835 line 199
  41. def OAI.MUB6.Certificate.PairSemantics.raw1835step0 line 201
  42. theorem OAI.MUB6.Certificate.PairSemantics.canonical1835 line 203
  43. def OAI.MUB6.Certificate.PairSemantics.raw1836 line 212
  44. def OAI.MUB6.Certificate.PairSemantics.raw1836step0 line 214
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical1836 line 216
  46. def OAI.MUB6.Certificate.PairSemantics.raw1837 line 225
  47. def OAI.MUB6.Certificate.PairSemantics.raw1837step0 line 227
  48. def OAI.MUB6.Certificate.PairSemantics.raw1837step1 line 229
  49. def OAI.MUB6.Certificate.PairSemantics.raw1837step2 line 231
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical1837 line 233
  51. def OAI.MUB6.Certificate.PairSemantics.raw1838 line 251
  52. def OAI.MUB6.Certificate.PairSemantics.raw1838step0 line 253
  53. theorem OAI.MUB6.Certificate.PairSemantics.canonical1838 line 255
  54. def OAI.MUB6.Certificate.PairSemantics.raw1839 line 264
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical1839 line 266
  56. def OAI.MUB6.Certificate.PairSemantics.raw1840 line 270
  57. theorem OAI.MUB6.Certificate.PairSemantics.canonical1840 line 272
  58. def OAI.MUB6.Certificate.PairSemantics.raw1841 line 276
  59. def OAI.MUB6.Certificate.PairSemantics.raw1841step0 line 278
  60. def OAI.MUB6.Certificate.PairSemantics.raw1841step1 line 280
  61. theorem OAI.MUB6.Certificate.PairSemantics.canonical1841 line 282
  62. def OAI.MUB6.Certificate.PairSemantics.raw1842 line 295
  63. def OAI.MUB6.Certificate.PairSemantics.raw1842step0 line 297
  64. theorem OAI.MUB6.Certificate.PairSemantics.canonical1842 line 299
  65. def OAI.MUB6.Certificate.PairSemantics.raw1843 line 308
  66. def OAI.MUB6.Certificate.PairSemantics.raw1843step0 line 310
  67. def OAI.MUB6.Certificate.PairSemantics.raw1843step1 line 312
  68. theorem OAI.MUB6.Certificate.PairSemantics.canonical1843 line 314
  69. def OAI.MUB6.Certificate.PairSemantics.raw1844 line 327
  70. def OAI.MUB6.Certificate.PairSemantics.raw1844step0 line 329
  71. theorem OAI.MUB6.Certificate.PairSemantics.canonical1844 line 331
  72. def OAI.MUB6.Certificate.PairSemantics.raw1845 line 340
  73. def OAI.MUB6.Certificate.PairSemantics.raw1845step0 line 342
  74. def OAI.MUB6.Certificate.PairSemantics.raw1845step1 line 344
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical1845 line 346
  76. def OAI.MUB6.Certificate.PairSemantics.raw1846 line 359
  77. theorem OAI.MUB6.Certificate.PairSemantics.canonical1846 line 361
  78. def OAI.MUB6.Certificate.PairSemantics.raw1847 line 365
  79. def OAI.MUB6.Certificate.PairSemantics.raw1847step0 line 367
  80. theorem OAI.MUB6.Certificate.PairSemantics.canonical1847 line 369
  81. def OAI.MUB6.Certificate.PairSemantics.raw1848 line 378
  82. def OAI.MUB6.Certificate.PairSemantics.raw1848step0 line 380
  83. theorem OAI.MUB6.Certificate.PairSemantics.canonical1848 line 382
  84. def OAI.MUB6.Certificate.PairSemantics.raw1849 line 391
  85. def OAI.MUB6.Certificate.PairSemantics.raw1849step0 line 393
  86. theorem OAI.MUB6.Certificate.PairSemantics.canonical1849 line 395
  87. def OAI.MUB6.Certificate.PairSemantics.raw1850 line 404
  88. def OAI.MUB6.Certificate.PairSemantics.raw1850step0 line 406
  89. theorem OAI.MUB6.Certificate.PairSemantics.canonical1850 line 408
  90. def OAI.MUB6.Certificate.PairSemantics.raw1851 line 417
  91. def OAI.MUB6.Certificate.PairSemantics.raw1851step0 line 419
  92. def OAI.MUB6.Certificate.PairSemantics.raw1851step1 line 421
  93. theorem OAI.MUB6.Certificate.PairSemantics.canonical1851 line 423
  94. def OAI.MUB6.Certificate.PairSemantics.raw1852 line 436
  95. def OAI.MUB6.Certificate.PairSemantics.raw1852step0 line 438
  96. def OAI.MUB6.Certificate.PairSemantics.raw1852step1 line 440
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical1852 line 442
  98. def OAI.MUB6.Certificate.PairSemantics.raw1853 line 455
  99. def OAI.MUB6.Certificate.PairSemantics.raw1853step0 line 457
  100. def OAI.MUB6.Certificate.PairSemantics.raw1853step1 line 459
  101. theorem OAI.MUB6.Certificate.PairSemantics.canonical1853 line 461
  102. def OAI.MUB6.Certificate.PairSemantics.raw1854 line 474
  103. theorem OAI.MUB6.Certificate.PairSemantics.canonical1854 line 476
  104. def OAI.MUB6.Certificate.PairSemantics.raw1855 line 480
  105. def OAI.MUB6.Certificate.PairSemantics.raw1855step0 line 482
  106. theorem OAI.MUB6.Certificate.PairSemantics.canonical1855 line 484