OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound28.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1792 line 78
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1792 line 84
3. theorem OAI.MUB6.Certificate.PairSemantics.sound1792 line 86
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1793 line 121
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1793 line 127
6. theorem OAI.MUB6.Certificate.PairSemantics.sound1793 line 129
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1794 line 164
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1794 line 170
9. theorem OAI.MUB6.Certificate.PairSemantics.sound1794 line 172
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1795 line 207
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1795 line 213
12. theorem OAI.MUB6.Certificate.PairSemantics.sound1795 line 215
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1796 line 250
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1796 line 256
15. theorem OAI.MUB6.Certificate.PairSemantics.sound1796 line 258
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1797 line 293
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1797 line 299
18. theorem OAI.MUB6.Certificate.PairSemantics.sound1797 line 301
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1798 line 336
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1798 line 342
21. theorem OAI.MUB6.Certificate.PairSemantics.sound1798 line 344
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1799 line 379
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1799 line 385
24. theorem OAI.MUB6.Certificate.PairSemantics.sound1799 line 387
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1800 line 422
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1800 line 428
27. theorem OAI.MUB6.Certificate.PairSemantics.sound1800 line 430
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1801 line 465
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1801 line 471
30. theorem OAI.MUB6.Certificate.PairSemantics.sound1801 line 473
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1802 line 508
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1802 line 514
33. theorem OAI.MUB6.Certificate.PairSemantics.sound1802 line 516
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1803 line 551
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1803 line 557
36. theorem OAI.MUB6.Certificate.PairSemantics.sound1803 line 559
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1804 line 594
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1804 line 600
39. theorem OAI.MUB6.Certificate.PairSemantics.sound1804 line 602
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1805 line 637
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1805 line 643
42. theorem OAI.MUB6.Certificate.PairSemantics.sound1805 line 645
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1806 line 680
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1806 line 686
45. theorem OAI.MUB6.Certificate.PairSemantics.sound1806 line 688
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1807 line 723
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1807 line 729
48. theorem OAI.MUB6.Certificate.PairSemantics.sound1807 line 731
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1808 line 766
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1808 line 772
51. theorem OAI.MUB6.Certificate.PairSemantics.sound1808 line 774
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1809 line 809
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1809 line 815
54. theorem OAI.MUB6.Certificate.PairSemantics.sound1809 line 817
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1810 line 852
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1810 line 858
57. theorem OAI.MUB6.Certificate.PairSemantics.sound1810 line 860
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1811 line 895
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1811 line 901
60. theorem OAI.MUB6.Certificate.PairSemantics.sound1811 line 903
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1812 line 938
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1812 line 944
63. theorem OAI.MUB6.Certificate.PairSemantics.sound1812 line 946
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1813 line 981
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1813 line 987
66. theorem OAI.MUB6.Certificate.PairSemantics.sound1813 line 989
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1814 line 1024
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1814 line 1030
69. theorem OAI.MUB6.Certificate.PairSemantics.sound1814 line 1032
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1815 line 1067
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1815 line 1073
72. theorem OAI.MUB6.Certificate.PairSemantics.sound1815 line 1075
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1816 line 1110
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1816 line 1116
75. theorem OAI.MUB6.Certificate.PairSemantics.sound1816 line 1118
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1817 line 1153
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1817 line 1159
78. theorem OAI.MUB6.Certificate.PairSemantics.sound1817 line 1161
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1818 line 1196
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1818 line 1202
81. theorem OAI.MUB6.Certificate.PairSemantics.sound1818 line 1204
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1819 line 1239
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1819 line 1245
84. theorem OAI.MUB6.Certificate.PairSemantics.sound1819 line 1247
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1820 line 1282
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1820 line 1288
87. theorem OAI.MUB6.Certificate.PairSemantics.sound1820 line 1290
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1821 line 1325
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1821 line 1331
90. theorem OAI.MUB6.Certificate.PairSemantics.sound1821 line 1333
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1822 line 1368
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1822 line 1374
93. theorem OAI.MUB6.Certificate.PairSemantics.sound1822 line 1376
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1823 line 1411
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1823 line 1417
96. theorem OAI.MUB6.Certificate.PairSemantics.sound1823 line 1419
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1824 line 1454
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1824 line 1460
99. theorem OAI.MUB6.Certificate.PairSemantics.sound1824 line 1462
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1825 line 1497
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1825 line 1503
102. theorem OAI.MUB6.Certificate.PairSemantics.sound1825 line 1505
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1826 line 1540
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1826 line 1546
105. theorem OAI.MUB6.Certificate.PairSemantics.sound1826 line 1548
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1827 line 1583
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1827 line 1589
108. theorem OAI.MUB6.Certificate.PairSemantics.sound1827 line 1591
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1828 line 1626
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1828 line 1632
111. theorem OAI.MUB6.Certificate.PairSemantics.sound1828 line 1634
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1829 line 1669
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1829 line 1675
114. theorem OAI.MUB6.Certificate.PairSemantics.sound1829 line 1677
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1830 line 1712
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1830 line 1718
117. theorem OAI.MUB6.Certificate.PairSemantics.sound1830 line 1720
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1831 line 1755
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1831 line 1761
120. theorem OAI.MUB6.Certificate.PairSemantics.sound1831 line 1763
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1832 line 1798
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1832 line 1804
123. theorem OAI.MUB6.Certificate.PairSemantics.sound1832 line 1806
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1833 line 1841
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1833 line 1847
126. theorem OAI.MUB6.Certificate.PairSemantics.sound1833 line 1849
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1834 line 1884
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1834 line 1890
129. theorem OAI.MUB6.Certificate.PairSemantics.sound1834 line 1892
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1835 line 1927
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1835 line 1933
132. theorem OAI.MUB6.Certificate.PairSemantics.sound1835 line 1935
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1836 line 1970
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1836 line 1976
135. theorem OAI.MUB6.Certificate.PairSemantics.sound1836 line 1978
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1837 line 2013
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1837 line 2019
138. theorem OAI.MUB6.Certificate.PairSemantics.sound1837 line 2021
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1838 line 2056
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1838 line 2062
141. theorem OAI.MUB6.Certificate.PairSemantics.sound1838 line 2064
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1839 line 2099
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1839 line 2105
144. theorem OAI.MUB6.Certificate.PairSemantics.sound1839 line 2107
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1840 line 2142
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1840 line 2148
147. theorem OAI.MUB6.Certificate.PairSemantics.sound1840 line 2150
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1841 line 2185
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1841 line 2191
150. theorem OAI.MUB6.Certificate.PairSemantics.sound1841 line 2193
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1842 line 2228
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1842 line 2234
153. theorem OAI.MUB6.Certificate.PairSemantics.sound1842 line 2236
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1843 line 2271
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1843 line 2277
156. theorem OAI.MUB6.Certificate.PairSemantics.sound1843 line 2279
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1844 line 2314
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1844 line 2320
159. theorem OAI.MUB6.Certificate.PairSemantics.sound1844 line 2322
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1845 line 2357
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1845 line 2363
162. theorem OAI.MUB6.Certificate.PairSemantics.sound1845 line 2365
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1846 line 2400
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1846 line 2406
165. theorem OAI.MUB6.Certificate.PairSemantics.sound1846 line 2408
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1847 line 2443
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1847 line 2449
168. theorem OAI.MUB6.Certificate.PairSemantics.sound1847 line 2451
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1848 line 2486
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1848 line 2492
171. theorem OAI.MUB6.Certificate.PairSemantics.sound1848 line 2494
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1849 line 2529
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1849 line 2535
174. theorem OAI.MUB6.Certificate.PairSemantics.sound1849 line 2537
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1850 line 2577
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1850 line 2583
177. theorem OAI.MUB6.Certificate.PairSemantics.sound1850 line 2585
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1851 line 2625
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1851 line 2631
180. theorem OAI.MUB6.Certificate.PairSemantics.sound1851 line 2633
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1852 line 2673
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1852 line 2679
183. theorem OAI.MUB6.Certificate.PairSemantics.sound1852 line 2681
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1853 line 2721
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1853 line 2727
186. theorem OAI.MUB6.Certificate.PairSemantics.sound1853 line 2729
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1854 line 2769
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1854 line 2775
189. theorem OAI.MUB6.Certificate.PairSemantics.sound1854 line 2777
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1855 line 2817
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1855 line 2823
192. theorem OAI.MUB6.Certificate.PairSemantics.sound1855 line 2825