OAI/Analysis/MutuallyUnbiased/MixedSemantics/Sources57.lean

GitHub source file

160 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MUB6.Certificate.MixedSemantics.sourceA1824 line 27
  2. def OAI.MUB6.Certificate.MixedSemantics.sourceB1824 line 28
  3. def OAI.MUB6.Certificate.MixedSemantics.sourceC1824 line 29
  4. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1824 line 30
  5. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1824 line 32
  6. def OAI.MUB6.Certificate.MixedSemantics.sourceA1825 line 83
  7. def OAI.MUB6.Certificate.MixedSemantics.sourceB1825 line 84
  8. def OAI.MUB6.Certificate.MixedSemantics.sourceC1825 line 85
  9. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1825 line 86
  10. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1825 line 88
  11. def OAI.MUB6.Certificate.MixedSemantics.sourceA1826 line 139
  12. def OAI.MUB6.Certificate.MixedSemantics.sourceB1826 line 140
  13. def OAI.MUB6.Certificate.MixedSemantics.sourceC1826 line 141
  14. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1826 line 142
  15. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1826 line 144
  16. def OAI.MUB6.Certificate.MixedSemantics.sourceA1827 line 195
  17. def OAI.MUB6.Certificate.MixedSemantics.sourceB1827 line 196
  18. def OAI.MUB6.Certificate.MixedSemantics.sourceC1827 line 197
  19. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1827 line 198
  20. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1827 line 200
  21. def OAI.MUB6.Certificate.MixedSemantics.sourceA1828 line 251
  22. def OAI.MUB6.Certificate.MixedSemantics.sourceB1828 line 252
  23. def OAI.MUB6.Certificate.MixedSemantics.sourceC1828 line 253
  24. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1828 line 254
  25. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1828 line 256
  26. def OAI.MUB6.Certificate.MixedSemantics.sourceA1829 line 307
  27. def OAI.MUB6.Certificate.MixedSemantics.sourceB1829 line 308
  28. def OAI.MUB6.Certificate.MixedSemantics.sourceC1829 line 309
  29. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1829 line 310
  30. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1829 line 312
  31. def OAI.MUB6.Certificate.MixedSemantics.sourceA1830 line 363
  32. def OAI.MUB6.Certificate.MixedSemantics.sourceB1830 line 364
  33. def OAI.MUB6.Certificate.MixedSemantics.sourceC1830 line 365
  34. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1830 line 366
  35. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1830 line 368
  36. def OAI.MUB6.Certificate.MixedSemantics.sourceA1831 line 419
  37. def OAI.MUB6.Certificate.MixedSemantics.sourceB1831 line 420
  38. def OAI.MUB6.Certificate.MixedSemantics.sourceC1831 line 421
  39. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1831 line 422
  40. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1831 line 424
  41. def OAI.MUB6.Certificate.MixedSemantics.sourceA1832 line 475
  42. def OAI.MUB6.Certificate.MixedSemantics.sourceB1832 line 476
  43. def OAI.MUB6.Certificate.MixedSemantics.sourceC1832 line 477
  44. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1832 line 478
  45. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1832 line 480
  46. def OAI.MUB6.Certificate.MixedSemantics.sourceA1833 line 531
  47. def OAI.MUB6.Certificate.MixedSemantics.sourceB1833 line 532
  48. def OAI.MUB6.Certificate.MixedSemantics.sourceC1833 line 533
  49. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1833 line 534
  50. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1833 line 536
  51. def OAI.MUB6.Certificate.MixedSemantics.sourceA1834 line 587
  52. def OAI.MUB6.Certificate.MixedSemantics.sourceB1834 line 588
  53. def OAI.MUB6.Certificate.MixedSemantics.sourceC1834 line 589
  54. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1834 line 590
  55. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1834 line 592
  56. def OAI.MUB6.Certificate.MixedSemantics.sourceA1835 line 643
  57. def OAI.MUB6.Certificate.MixedSemantics.sourceB1835 line 644
  58. def OAI.MUB6.Certificate.MixedSemantics.sourceC1835 line 645
  59. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1835 line 646
  60. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1835 line 648
  61. def OAI.MUB6.Certificate.MixedSemantics.sourceA1836 line 699
  62. def OAI.MUB6.Certificate.MixedSemantics.sourceB1836 line 700
  63. def OAI.MUB6.Certificate.MixedSemantics.sourceC1836 line 701
  64. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1836 line 702
  65. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1836 line 704
  66. def OAI.MUB6.Certificate.MixedSemantics.sourceA1837 line 755
  67. def OAI.MUB6.Certificate.MixedSemantics.sourceB1837 line 756
  68. def OAI.MUB6.Certificate.MixedSemantics.sourceC1837 line 757
  69. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1837 line 758
  70. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1837 line 760
  71. def OAI.MUB6.Certificate.MixedSemantics.sourceA1838 line 811
  72. def OAI.MUB6.Certificate.MixedSemantics.sourceB1838 line 812
  73. def OAI.MUB6.Certificate.MixedSemantics.sourceC1838 line 813
  74. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1838 line 814
  75. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1838 line 816
  76. def OAI.MUB6.Certificate.MixedSemantics.sourceA1839 line 867
  77. def OAI.MUB6.Certificate.MixedSemantics.sourceB1839 line 868
  78. def OAI.MUB6.Certificate.MixedSemantics.sourceC1839 line 869
  79. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1839 line 870
  80. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1839 line 872
  81. def OAI.MUB6.Certificate.MixedSemantics.sourceA1840 line 923
  82. def OAI.MUB6.Certificate.MixedSemantics.sourceB1840 line 924
  83. def OAI.MUB6.Certificate.MixedSemantics.sourceC1840 line 925
  84. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1840 line 926
  85. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1840 line 928
  86. def OAI.MUB6.Certificate.MixedSemantics.sourceA1841 line 979
  87. def OAI.MUB6.Certificate.MixedSemantics.sourceB1841 line 980
  88. def OAI.MUB6.Certificate.MixedSemantics.sourceC1841 line 981
  89. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1841 line 982
  90. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1841 line 984
  91. def OAI.MUB6.Certificate.MixedSemantics.sourceA1842 line 1035
  92. def OAI.MUB6.Certificate.MixedSemantics.sourceB1842 line 1036
  93. def OAI.MUB6.Certificate.MixedSemantics.sourceC1842 line 1037
  94. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1842 line 1038
  95. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1842 line 1040
  96. def OAI.MUB6.Certificate.MixedSemantics.sourceA1843 line 1091
  97. def OAI.MUB6.Certificate.MixedSemantics.sourceB1843 line 1092
  98. def OAI.MUB6.Certificate.MixedSemantics.sourceC1843 line 1093
  99. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1843 line 1094
  100. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1843 line 1096
  101. def OAI.MUB6.Certificate.MixedSemantics.sourceA1844 line 1285
  102. def OAI.MUB6.Certificate.MixedSemantics.sourceB1844 line 1286
  103. def OAI.MUB6.Certificate.MixedSemantics.sourceC1844 line 1287
  104. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1844 line 1288
  105. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1844 line 1290
  106. def OAI.MUB6.Certificate.MixedSemantics.sourceA1845 line 1479
  107. def OAI.MUB6.Certificate.MixedSemantics.sourceB1845 line 1480
  108. def OAI.MUB6.Certificate.MixedSemantics.sourceC1845 line 1481
  109. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1845 line 1482
  110. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1845 line 1484
  111. def OAI.MUB6.Certificate.MixedSemantics.sourceA1846 line 1673
  112. def OAI.MUB6.Certificate.MixedSemantics.sourceB1846 line 1674
  113. def OAI.MUB6.Certificate.MixedSemantics.sourceC1846 line 1675
  114. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1846 line 1676
  115. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1846 line 1678
  116. def OAI.MUB6.Certificate.MixedSemantics.sourceA1847 line 1867
  117. def OAI.MUB6.Certificate.MixedSemantics.sourceB1847 line 1868
  118. def OAI.MUB6.Certificate.MixedSemantics.sourceC1847 line 1869
  119. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1847 line 1870
  120. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1847 line 1872
  121. def OAI.MUB6.Certificate.MixedSemantics.sourceA1848 line 2061
  122. def OAI.MUB6.Certificate.MixedSemantics.sourceB1848 line 2062
  123. def OAI.MUB6.Certificate.MixedSemantics.sourceC1848 line 2063
  124. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1848 line 2064
  125. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1848 line 2066
  126. def OAI.MUB6.Certificate.MixedSemantics.sourceA1849 line 2117
  127. def OAI.MUB6.Certificate.MixedSemantics.sourceB1849 line 2118
  128. def OAI.MUB6.Certificate.MixedSemantics.sourceC1849 line 2119
  129. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1849 line 2120
  130. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1849 line 2122
  131. def OAI.MUB6.Certificate.MixedSemantics.sourceA1850 line 2311
  132. def OAI.MUB6.Certificate.MixedSemantics.sourceB1850 line 2312
  133. def OAI.MUB6.Certificate.MixedSemantics.sourceC1850 line 2313
  134. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1850 line 2314
  135. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1850 line 2316
  136. def OAI.MUB6.Certificate.MixedSemantics.sourceA1851 line 2505
  137. def OAI.MUB6.Certificate.MixedSemantics.sourceB1851 line 2506
  138. def OAI.MUB6.Certificate.MixedSemantics.sourceC1851 line 2507
  139. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1851 line 2508
  140. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1851 line 2510
  141. def OAI.MUB6.Certificate.MixedSemantics.sourceA1852 line 2561
  142. def OAI.MUB6.Certificate.MixedSemantics.sourceB1852 line 2562
  143. def OAI.MUB6.Certificate.MixedSemantics.sourceC1852 line 2563
  144. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1852 line 2564
  145. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1852 line 2566
  146. def OAI.MUB6.Certificate.MixedSemantics.sourceA1853 line 2755
  147. def OAI.MUB6.Certificate.MixedSemantics.sourceB1853 line 2756
  148. def OAI.MUB6.Certificate.MixedSemantics.sourceC1853 line 2757
  149. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1853 line 2758
  150. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1853 line 2760
  151. def OAI.MUB6.Certificate.MixedSemantics.sourceA1854 line 2949
  152. def OAI.MUB6.Certificate.MixedSemantics.sourceB1854 line 2950
  153. def OAI.MUB6.Certificate.MixedSemantics.sourceC1854 line 2951
  154. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1854 line 2952
  155. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1854 line 2954
  156. def OAI.MUB6.Certificate.MixedSemantics.sourceA1855 line 3143
  157. def OAI.MUB6.Certificate.MixedSemantics.sourceB1855 line 3144
  158. def OAI.MUB6.Certificate.MixedSemantics.sourceC1855 line 3145
  159. def OAI.MUB6.Certificate.MixedSemantics.sourceForm1855 line 3146
  160. theorem OAI.MUB6.Certificate.MixedSemantics.sourceEq1855 line 3148