OAI/Analysis/MutuallyUnbiased/PairSemantics/Canonical58.lean

GitHub source file

127 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.PairSemantics.raw1856 line 18
  2. def OAI.MUB6.Certificate.PairSemantics.raw1856step0 line 20
  3. def OAI.MUB6.Certificate.PairSemantics.raw1856step1 line 22
  4. theorem OAI.MUB6.Certificate.PairSemantics.canonical1856 line 24
  5. def OAI.MUB6.Certificate.PairSemantics.raw1857 line 37
  6. def OAI.MUB6.Certificate.PairSemantics.raw1857step0 line 39
  7. def OAI.MUB6.Certificate.PairSemantics.raw1857step1 line 41
  8. theorem OAI.MUB6.Certificate.PairSemantics.canonical1857 line 43
  9. def OAI.MUB6.Certificate.PairSemantics.raw1858 line 56
  10. def OAI.MUB6.Certificate.PairSemantics.raw1858step0 line 58
  11. def OAI.MUB6.Certificate.PairSemantics.raw1858step1 line 60
  12. theorem OAI.MUB6.Certificate.PairSemantics.canonical1858 line 62
  13. def OAI.MUB6.Certificate.PairSemantics.raw1859 line 75
  14. def OAI.MUB6.Certificate.PairSemantics.raw1859step0 line 77
  15. def OAI.MUB6.Certificate.PairSemantics.raw1859step1 line 79
  16. theorem OAI.MUB6.Certificate.PairSemantics.canonical1859 line 81
  17. def OAI.MUB6.Certificate.PairSemantics.raw1860 line 94
  18. def OAI.MUB6.Certificate.PairSemantics.raw1860step0 line 96
  19. theorem OAI.MUB6.Certificate.PairSemantics.canonical1860 line 98
  20. def OAI.MUB6.Certificate.PairSemantics.raw1861 line 107
  21. def OAI.MUB6.Certificate.PairSemantics.raw1861step0 line 109
  22. def OAI.MUB6.Certificate.PairSemantics.raw1861step1 line 111
  23. def OAI.MUB6.Certificate.PairSemantics.raw1861step2 line 113
  24. theorem OAI.MUB6.Certificate.PairSemantics.canonical1861 line 115
  25. def OAI.MUB6.Certificate.PairSemantics.raw1862 line 133
  26. def OAI.MUB6.Certificate.PairSemantics.raw1862step0 line 135
  27. def OAI.MUB6.Certificate.PairSemantics.raw1862step1 line 137
  28. def OAI.MUB6.Certificate.PairSemantics.raw1862step2 line 139
  29. def OAI.MUB6.Certificate.PairSemantics.raw1862step3 line 141
  30. theorem OAI.MUB6.Certificate.PairSemantics.canonical1862 line 143
  31. def OAI.MUB6.Certificate.PairSemantics.raw1863 line 165
  32. def OAI.MUB6.Certificate.PairSemantics.raw1863step0 line 167
  33. def OAI.MUB6.Certificate.PairSemantics.raw1863step1 line 169
  34. def OAI.MUB6.Certificate.PairSemantics.raw1863step2 line 171
  35. def OAI.MUB6.Certificate.PairSemantics.raw1863step3 line 173
  36. theorem OAI.MUB6.Certificate.PairSemantics.canonical1863 line 175
  37. def OAI.MUB6.Certificate.PairSemantics.raw1864 line 197
  38. def OAI.MUB6.Certificate.PairSemantics.raw1864step0 line 199
  39. def OAI.MUB6.Certificate.PairSemantics.raw1864step1 line 201
  40. def OAI.MUB6.Certificate.PairSemantics.raw1864step2 line 203
  41. theorem OAI.MUB6.Certificate.PairSemantics.canonical1864 line 205
  42. def OAI.MUB6.Certificate.PairSemantics.raw1865 line 223
  43. def OAI.MUB6.Certificate.PairSemantics.raw1865step0 line 225
  44. def OAI.MUB6.Certificate.PairSemantics.raw1865step1 line 227
  45. theorem OAI.MUB6.Certificate.PairSemantics.canonical1865 line 229
  46. def OAI.MUB6.Certificate.PairSemantics.raw1866 line 243
  47. def OAI.MUB6.Certificate.PairSemantics.raw1866step0 line 245
  48. def OAI.MUB6.Certificate.PairSemantics.raw1866step1 line 247
  49. def OAI.MUB6.Certificate.PairSemantics.raw1866step2 line 249
  50. theorem OAI.MUB6.Certificate.PairSemantics.canonical1866 line 251
  51. def OAI.MUB6.Certificate.PairSemantics.raw1867 line 269
  52. def OAI.MUB6.Certificate.PairSemantics.raw1867step0 line 271
  53. def OAI.MUB6.Certificate.PairSemantics.raw1867step1 line 273
  54. def OAI.MUB6.Certificate.PairSemantics.raw1867step2 line 275
  55. theorem OAI.MUB6.Certificate.PairSemantics.canonical1867 line 277
  56. def OAI.MUB6.Certificate.PairSemantics.raw1868 line 295
  57. def OAI.MUB6.Certificate.PairSemantics.raw1868step0 line 297
  58. def OAI.MUB6.Certificate.PairSemantics.raw1868step1 line 299
  59. def OAI.MUB6.Certificate.PairSemantics.raw1868step2 line 301
  60. theorem OAI.MUB6.Certificate.PairSemantics.canonical1868 line 303
  61. def OAI.MUB6.Certificate.PairSemantics.raw1869 line 321
  62. def OAI.MUB6.Certificate.PairSemantics.raw1869step0 line 323
  63. def OAI.MUB6.Certificate.PairSemantics.raw1869step1 line 325
  64. def OAI.MUB6.Certificate.PairSemantics.raw1869step2 line 327
  65. def OAI.MUB6.Certificate.PairSemantics.raw1869step3 line 329
  66. theorem OAI.MUB6.Certificate.PairSemantics.canonical1869 line 331
  67. def OAI.MUB6.Certificate.PairSemantics.raw1870 line 353
  68. def OAI.MUB6.Certificate.PairSemantics.raw1870step0 line 355
  69. theorem OAI.MUB6.Certificate.PairSemantics.canonical1870 line 357
  70. def OAI.MUB6.Certificate.PairSemantics.raw1871 line 366
  71. def OAI.MUB6.Certificate.PairSemantics.raw1871step0 line 368
  72. theorem OAI.MUB6.Certificate.PairSemantics.canonical1871 line 370
  73. def OAI.MUB6.Certificate.PairSemantics.raw1872 line 379
  74. def OAI.MUB6.Certificate.PairSemantics.raw1872step0 line 381
  75. theorem OAI.MUB6.Certificate.PairSemantics.canonical1872 line 383
  76. def OAI.MUB6.Certificate.PairSemantics.raw1873 line 392
  77. def OAI.MUB6.Certificate.PairSemantics.raw1873step0 line 394
  78. theorem OAI.MUB6.Certificate.PairSemantics.canonical1873 line 396
  79. def OAI.MUB6.Certificate.PairSemantics.raw1874 line 405
  80. def OAI.MUB6.Certificate.PairSemantics.raw1874step0 line 407
  81. def OAI.MUB6.Certificate.PairSemantics.raw1874step1 line 409
  82. theorem OAI.MUB6.Certificate.PairSemantics.canonical1874 line 411
  83. def OAI.MUB6.Certificate.PairSemantics.raw1875 line 425
  84. def OAI.MUB6.Certificate.PairSemantics.raw1875step0 line 427
  85. def OAI.MUB6.Certificate.PairSemantics.raw1875step1 line 429
  86. def OAI.MUB6.Certificate.PairSemantics.raw1875step2 line 431
  87. theorem OAI.MUB6.Certificate.PairSemantics.canonical1875 line 433
  88. def OAI.MUB6.Certificate.PairSemantics.raw1876 line 451
  89. def OAI.MUB6.Certificate.PairSemantics.raw1876step0 line 453
  90. def OAI.MUB6.Certificate.PairSemantics.raw1876step1 line 455
  91. def OAI.MUB6.Certificate.PairSemantics.raw1876step2 line 457
  92. theorem OAI.MUB6.Certificate.PairSemantics.canonical1876 line 459
  93. def OAI.MUB6.Certificate.PairSemantics.raw1877 line 477
  94. def OAI.MUB6.Certificate.PairSemantics.raw1877step0 line 479
  95. def OAI.MUB6.Certificate.PairSemantics.raw1877step1 line 481
  96. def OAI.MUB6.Certificate.PairSemantics.raw1877step2 line 483
  97. theorem OAI.MUB6.Certificate.PairSemantics.canonical1877 line 485
  98. def OAI.MUB6.Certificate.PairSemantics.raw1878 line 503
  99. def OAI.MUB6.Certificate.PairSemantics.raw1878step0 line 505
  100. theorem OAI.MUB6.Certificate.PairSemantics.canonical1878 line 507
  101. def OAI.MUB6.Certificate.PairSemantics.raw1879 line 516
  102. def OAI.MUB6.Certificate.PairSemantics.raw1879step0 line 518
  103. def OAI.MUB6.Certificate.PairSemantics.raw1879step1 line 520
  104. def OAI.MUB6.Certificate.PairSemantics.raw1879step2 line 522
  105. theorem OAI.MUB6.Certificate.PairSemantics.canonical1879 line 524
  106. def OAI.MUB6.Certificate.PairSemantics.raw1880 line 542
  107. def OAI.MUB6.Certificate.PairSemantics.raw1880step0 line 544
  108. theorem OAI.MUB6.Certificate.PairSemantics.canonical1880 line 546
  109. def OAI.MUB6.Certificate.PairSemantics.raw1881 line 555
  110. def OAI.MUB6.Certificate.PairSemantics.raw1881step0 line 557
  111. theorem OAI.MUB6.Certificate.PairSemantics.canonical1881 line 559
  112. def OAI.MUB6.Certificate.PairSemantics.raw1882 line 568
  113. theorem OAI.MUB6.Certificate.PairSemantics.canonical1882 line 570
  114. def OAI.MUB6.Certificate.PairSemantics.raw1883 line 574
  115. theorem OAI.MUB6.Certificate.PairSemantics.canonical1883 line 576
  116. def OAI.MUB6.Certificate.PairSemantics.raw1884 line 580
  117. theorem OAI.MUB6.Certificate.PairSemantics.canonical1884 line 582
  118. def OAI.MUB6.Certificate.PairSemantics.raw1885 line 586
  119. def OAI.MUB6.Certificate.PairSemantics.raw1885step0 line 588
  120. theorem OAI.MUB6.Certificate.PairSemantics.canonical1885 line 590
  121. def OAI.MUB6.Certificate.PairSemantics.raw1886 line 599
  122. def OAI.MUB6.Certificate.PairSemantics.raw1886step0 line 601
  123. theorem OAI.MUB6.Certificate.PairSemantics.canonical1886 line 603
  124. def OAI.MUB6.Certificate.PairSemantics.raw1887 line 612
  125. def OAI.MUB6.Certificate.PairSemantics.raw1887step0 line 614
  126. def OAI.MUB6.Certificate.PairSemantics.raw1887step1 line 616
  127. theorem OAI.MUB6.Certificate.PairSemantics.canonical1887 line 618