OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound29.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1856 line 95
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1856 line 101
3. theorem OAI.MUB6.Certificate.PairSemantics.sound1856 line 103
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1857 line 143
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1857 line 149
6. theorem OAI.MUB6.Certificate.PairSemantics.sound1857 line 151
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1858 line 191
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1858 line 197
9. theorem OAI.MUB6.Certificate.PairSemantics.sound1858 line 199
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1859 line 239
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1859 line 245
12. theorem OAI.MUB6.Certificate.PairSemantics.sound1859 line 247
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1860 line 287
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1860 line 293
15. theorem OAI.MUB6.Certificate.PairSemantics.sound1860 line 295
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1861 line 335
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1861 line 341
18. theorem OAI.MUB6.Certificate.PairSemantics.sound1861 line 343
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1862 line 383
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1862 line 389
21. theorem OAI.MUB6.Certificate.PairSemantics.sound1862 line 391
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1863 line 431
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1863 line 437
24. theorem OAI.MUB6.Certificate.PairSemantics.sound1863 line 439
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1864 line 479
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1864 line 485
27. theorem OAI.MUB6.Certificate.PairSemantics.sound1864 line 487
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1865 line 527
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1865 line 533
30. theorem OAI.MUB6.Certificate.PairSemantics.sound1865 line 535
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1866 line 575
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1866 line 581
33. theorem OAI.MUB6.Certificate.PairSemantics.sound1866 line 583
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1867 line 623
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1867 line 629
36. theorem OAI.MUB6.Certificate.PairSemantics.sound1867 line 631
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1868 line 671
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1868 line 677
39. theorem OAI.MUB6.Certificate.PairSemantics.sound1868 line 679
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1869 line 719
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1869 line 725
42. theorem OAI.MUB6.Certificate.PairSemantics.sound1869 line 727
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1870 line 767
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1870 line 773
45. theorem OAI.MUB6.Certificate.PairSemantics.sound1870 line 775
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1871 line 815
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1871 line 821
48. theorem OAI.MUB6.Certificate.PairSemantics.sound1871 line 823
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1872 line 863
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1872 line 869
51. theorem OAI.MUB6.Certificate.PairSemantics.sound1872 line 871
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1873 line 911
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1873 line 917
54. theorem OAI.MUB6.Certificate.PairSemantics.sound1873 line 919
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1874 line 959
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1874 line 965
57. theorem OAI.MUB6.Certificate.PairSemantics.sound1874 line 967
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1875 line 1007
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1875 line 1013
60. theorem OAI.MUB6.Certificate.PairSemantics.sound1875 line 1015
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1876 line 1055
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1876 line 1061
63. theorem OAI.MUB6.Certificate.PairSemantics.sound1876 line 1063
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1877 line 1103
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1877 line 1109
66. theorem OAI.MUB6.Certificate.PairSemantics.sound1877 line 1111
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1878 line 1151
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1878 line 1157
69. theorem OAI.MUB6.Certificate.PairSemantics.sound1878 line 1159
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1879 line 1199
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1879 line 1205
72. theorem OAI.MUB6.Certificate.PairSemantics.sound1879 line 1207
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1880 line 1247
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1880 line 1253
75. theorem OAI.MUB6.Certificate.PairSemantics.sound1880 line 1255
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1881 line 1295
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1881 line 1301
78. theorem OAI.MUB6.Certificate.PairSemantics.sound1881 line 1303
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1882 line 1343
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1882 line 1349
81. theorem OAI.MUB6.Certificate.PairSemantics.sound1882 line 1351
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1883 line 1391
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1883 line 1397
84. theorem OAI.MUB6.Certificate.PairSemantics.sound1883 line 1399
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1884 line 1439
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1884 line 1445
87. theorem OAI.MUB6.Certificate.PairSemantics.sound1884 line 1447
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1885 line 1487
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1885 line 1493
90. theorem OAI.MUB6.Certificate.PairSemantics.sound1885 line 1495
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1886 line 1535
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1886 line 1541
93. theorem OAI.MUB6.Certificate.PairSemantics.sound1886 line 1543
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1887 line 1583
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1887 line 1589
96. theorem OAI.MUB6.Certificate.PairSemantics.sound1887 line 1591
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1888 line 1631
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1888 line 1637
99. theorem OAI.MUB6.Certificate.PairSemantics.sound1888 line 1639
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1889 line 1679
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1889 line 1685
102. theorem OAI.MUB6.Certificate.PairSemantics.sound1889 line 1687
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1890 line 1727
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1890 line 1733
105. theorem OAI.MUB6.Certificate.PairSemantics.sound1890 line 1735
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1891 line 1775
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1891 line 1781
108. theorem OAI.MUB6.Certificate.PairSemantics.sound1891 line 1783
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1892 line 1823
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1892 line 1829
111. theorem OAI.MUB6.Certificate.PairSemantics.sound1892 line 1831
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1893 line 1866
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1893 line 1872
114. theorem OAI.MUB6.Certificate.PairSemantics.sound1893 line 1874
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1894 line 1909
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1894 line 1915
117. theorem OAI.MUB6.Certificate.PairSemantics.sound1894 line 1917
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1895 line 1952
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1895 line 1958
120. theorem OAI.MUB6.Certificate.PairSemantics.sound1895 line 1960
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1896 line 1995
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1896 line 2001
123. theorem OAI.MUB6.Certificate.PairSemantics.sound1896 line 2003
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1897 line 2038
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1897 line 2044
126. theorem OAI.MUB6.Certificate.PairSemantics.sound1897 line 2046
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1898 line 2081
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1898 line 2087
129. theorem OAI.MUB6.Certificate.PairSemantics.sound1898 line 2089
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1899 line 2124
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1899 line 2130
132. theorem OAI.MUB6.Certificate.PairSemantics.sound1899 line 2132
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1900 line 2167
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1900 line 2173
135. theorem OAI.MUB6.Certificate.PairSemantics.sound1900 line 2175
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1901 line 2210
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1901 line 2216
138. theorem OAI.MUB6.Certificate.PairSemantics.sound1901 line 2218
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1902 line 2253
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1902 line 2259
141. theorem OAI.MUB6.Certificate.PairSemantics.sound1902 line 2261
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1903 line 2296
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1903 line 2302
144. theorem OAI.MUB6.Certificate.PairSemantics.sound1903 line 2304
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1904 line 2339
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1904 line 2345
147. theorem OAI.MUB6.Certificate.PairSemantics.sound1904 line 2347
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1905 line 2382
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1905 line 2388
150. theorem OAI.MUB6.Certificate.PairSemantics.sound1905 line 2390
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1906 line 2425
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1906 line 2431
153. theorem OAI.MUB6.Certificate.PairSemantics.sound1906 line 2433
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1907 line 2468
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1907 line 2474
156. theorem OAI.MUB6.Certificate.PairSemantics.sound1907 line 2476
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1908 line 2511
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1908 line 2517
159. theorem OAI.MUB6.Certificate.PairSemantics.sound1908 line 2519
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1909 line 2554
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1909 line 2560
162. theorem OAI.MUB6.Certificate.PairSemantics.sound1909 line 2562
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1910 line 2597
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1910 line 2603
165. theorem OAI.MUB6.Certificate.PairSemantics.sound1910 line 2605
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1911 line 2640
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1911 line 2646
168. theorem OAI.MUB6.Certificate.PairSemantics.sound1911 line 2648
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1912 line 2683
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1912 line 2689
171. theorem OAI.MUB6.Certificate.PairSemantics.sound1912 line 2691
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1913 line 2726
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1913 line 2732
174. theorem OAI.MUB6.Certificate.PairSemantics.sound1913 line 2734
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1914 line 2769
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1914 line 2775
177. theorem OAI.MUB6.Certificate.PairSemantics.sound1914 line 2777
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1915 line 2812
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1915 line 2818
180. theorem OAI.MUB6.Certificate.PairSemantics.sound1915 line 2820
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1916 line 2855
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1916 line 2861
183. theorem OAI.MUB6.Certificate.PairSemantics.sound1916 line 2863
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1917 line 2898
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1917 line 2904
186. theorem OAI.MUB6.Certificate.PairSemantics.sound1917 line 2906
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1918 line 2941
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1918 line 2947
189. theorem OAI.MUB6.Certificate.PairSemantics.sound1918 line 2949
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1919 line 2984
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1919 line 2990
192. theorem OAI.MUB6.Certificate.PairSemantics.sound1919 line 2992