OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound31.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1984 line 86
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1984 line 92
3. theorem OAI.MUB6.Certificate.PairSemantics.sound1984 line 94
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1985 line 129
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1985 line 135
6. theorem OAI.MUB6.Certificate.PairSemantics.sound1985 line 137
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1986 line 172
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1986 line 178
9. theorem OAI.MUB6.Certificate.PairSemantics.sound1986 line 180
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1987 line 215
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1987 line 221
12. theorem OAI.MUB6.Certificate.PairSemantics.sound1987 line 223
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1988 line 258
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1988 line 264
15. theorem OAI.MUB6.Certificate.PairSemantics.sound1988 line 266
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1989 line 301
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1989 line 307
18. theorem OAI.MUB6.Certificate.PairSemantics.sound1989 line 309
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1990 line 344
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1990 line 350
21. theorem OAI.MUB6.Certificate.PairSemantics.sound1990 line 352
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1991 line 387
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1991 line 393
24. theorem OAI.MUB6.Certificate.PairSemantics.sound1991 line 395
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1992 line 430
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1992 line 436
27. theorem OAI.MUB6.Certificate.PairSemantics.sound1992 line 438
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1993 line 473
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1993 line 479
30. theorem OAI.MUB6.Certificate.PairSemantics.sound1993 line 481
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1994 line 516
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1994 line 522
33. theorem OAI.MUB6.Certificate.PairSemantics.sound1994 line 524
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1995 line 559
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1995 line 565
36. theorem OAI.MUB6.Certificate.PairSemantics.sound1995 line 567
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1996 line 602
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1996 line 608
39. theorem OAI.MUB6.Certificate.PairSemantics.sound1996 line 610
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1997 line 645
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1997 line 651
42. theorem OAI.MUB6.Certificate.PairSemantics.sound1997 line 653
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1998 line 688
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1998 line 694
45. theorem OAI.MUB6.Certificate.PairSemantics.sound1998 line 696
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1999 line 731
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1999 line 737
48. theorem OAI.MUB6.Certificate.PairSemantics.sound1999 line 739
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2000 line 774
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2000 line 780
51. theorem OAI.MUB6.Certificate.PairSemantics.sound2000 line 782
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2001 line 817
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2001 line 823
54. theorem OAI.MUB6.Certificate.PairSemantics.sound2001 line 825
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2002 line 860
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2002 line 866
57. theorem OAI.MUB6.Certificate.PairSemantics.sound2002 line 868
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2003 line 903
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2003 line 909
60. theorem OAI.MUB6.Certificate.PairSemantics.sound2003 line 911
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2004 line 946
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2004 line 952
63. theorem OAI.MUB6.Certificate.PairSemantics.sound2004 line 954
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2005 line 989
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2005 line 995
66. theorem OAI.MUB6.Certificate.PairSemantics.sound2005 line 997
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2006 line 1032
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2006 line 1038
69. theorem OAI.MUB6.Certificate.PairSemantics.sound2006 line 1040
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2007 line 1075
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2007 line 1081
72. theorem OAI.MUB6.Certificate.PairSemantics.sound2007 line 1083
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2008 line 1118
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2008 line 1124
75. theorem OAI.MUB6.Certificate.PairSemantics.sound2008 line 1126
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2009 line 1161
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2009 line 1167
78. theorem OAI.MUB6.Certificate.PairSemantics.sound2009 line 1169
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2010 line 1204
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2010 line 1210
81. theorem OAI.MUB6.Certificate.PairSemantics.sound2010 line 1212
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2011 line 1247
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2011 line 1253
84. theorem OAI.MUB6.Certificate.PairSemantics.sound2011 line 1255
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2012 line 1290
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2012 line 1296
87. theorem OAI.MUB6.Certificate.PairSemantics.sound2012 line 1298
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2013 line 1333
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2013 line 1339
90. theorem OAI.MUB6.Certificate.PairSemantics.sound2013 line 1341
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2014 line 1376
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2014 line 1382
93. theorem OAI.MUB6.Certificate.PairSemantics.sound2014 line 1384
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2015 line 1419
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2015 line 1425
96. theorem OAI.MUB6.Certificate.PairSemantics.sound2015 line 1427
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2016 line 1462
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2016 line 1468
99. theorem OAI.MUB6.Certificate.PairSemantics.sound2016 line 1470
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2017 line 1505
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2017 line 1511
102. theorem OAI.MUB6.Certificate.PairSemantics.sound2017 line 1513
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2018 line 1548
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2018 line 1554
105. theorem OAI.MUB6.Certificate.PairSemantics.sound2018 line 1556
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2019 line 1591
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2019 line 1597
108. theorem OAI.MUB6.Certificate.PairSemantics.sound2019 line 1599
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2020 line 1634
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2020 line 1640
111. theorem OAI.MUB6.Certificate.PairSemantics.sound2020 line 1642
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2021 line 1677
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2021 line 1683
114. theorem OAI.MUB6.Certificate.PairSemantics.sound2021 line 1685
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2022 line 1720
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2022 line 1726
117. theorem OAI.MUB6.Certificate.PairSemantics.sound2022 line 1728
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2023 line 1763
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2023 line 1769
120. theorem OAI.MUB6.Certificate.PairSemantics.sound2023 line 1771
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2024 line 1806
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2024 line 1812
123. theorem OAI.MUB6.Certificate.PairSemantics.sound2024 line 1814
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2025 line 1849
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2025 line 1855
126. theorem OAI.MUB6.Certificate.PairSemantics.sound2025 line 1857
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2026 line 1892
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2026 line 1898
129. theorem OAI.MUB6.Certificate.PairSemantics.sound2026 line 1900
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2027 line 1935
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2027 line 1941
132. theorem OAI.MUB6.Certificate.PairSemantics.sound2027 line 1943
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2028 line 1978
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2028 line 1984
135. theorem OAI.MUB6.Certificate.PairSemantics.sound2028 line 1986
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2029 line 2021
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2029 line 2027
138. theorem OAI.MUB6.Certificate.PairSemantics.sound2029 line 2029
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2030 line 2064
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2030 line 2070
141. theorem OAI.MUB6.Certificate.PairSemantics.sound2030 line 2072
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2031 line 2107
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2031 line 2113
144. theorem OAI.MUB6.Certificate.PairSemantics.sound2031 line 2115
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2032 line 2150
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2032 line 2156
147. theorem OAI.MUB6.Certificate.PairSemantics.sound2032 line 2158
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2033 line 2193
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2033 line 2199
150. theorem OAI.MUB6.Certificate.PairSemantics.sound2033 line 2201
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2034 line 2236
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2034 line 2242
153. theorem OAI.MUB6.Certificate.PairSemantics.sound2034 line 2244
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2035 line 2279
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2035 line 2285
156. theorem OAI.MUB6.Certificate.PairSemantics.sound2035 line 2287
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2036 line 2322
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2036 line 2328
159. theorem OAI.MUB6.Certificate.PairSemantics.sound2036 line 2330
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2037 line 2365
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2037 line 2371
162. theorem OAI.MUB6.Certificate.PairSemantics.sound2037 line 2373
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2038 line 2408
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2038 line 2414
165. theorem OAI.MUB6.Certificate.PairSemantics.sound2038 line 2416
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2039 line 2451
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2039 line 2457
168. theorem OAI.MUB6.Certificate.PairSemantics.sound2039 line 2459
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2040 line 2494
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2040 line 2500
171. theorem OAI.MUB6.Certificate.PairSemantics.sound2040 line 2502
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2041 line 2537
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2041 line 2543
174. theorem OAI.MUB6.Certificate.PairSemantics.sound2041 line 2545
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2042 line 2580
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2042 line 2586
177. theorem OAI.MUB6.Certificate.PairSemantics.sound2042 line 2588
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2043 line 2623
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2043 line 2629
180. theorem OAI.MUB6.Certificate.PairSemantics.sound2043 line 2631
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2044 line 2666
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2044 line 2672
183. theorem OAI.MUB6.Certificate.PairSemantics.sound2044 line 2674
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2045 line 2709
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2045 line 2715
186. theorem OAI.MUB6.Certificate.PairSemantics.sound2045 line 2717
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2046 line 2752
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2046 line 2758
189. theorem OAI.MUB6.Certificate.PairSemantics.sound2046 line 2760
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2047 line 2795
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2047 line 2801
192. theorem OAI.MUB6.Certificate.PairSemantics.sound2047 line 2803