OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound14.lean

GitHub source file

186 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation896 line 63
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix896 line 69
3. theorem OAI.MUB6.Certificate.PairSemantics.sound896 line 71
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation897 line 102
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix897 line 108
6. theorem OAI.MUB6.Certificate.PairSemantics.sound897 line 110
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation898 line 140
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix898 line 146
9. theorem OAI.MUB6.Certificate.PairSemantics.sound898 line 148
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation899 line 178
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix899 line 184
12. theorem OAI.MUB6.Certificate.PairSemantics.sound899 line 186
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation900 line 216
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix900 line 222
15. theorem OAI.MUB6.Certificate.PairSemantics.sound900 line 224
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation901 line 255
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix901 line 261
18. theorem OAI.MUB6.Certificate.PairSemantics.sound901 line 263
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation902 line 294
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix902 line 300
21. theorem OAI.MUB6.Certificate.PairSemantics.sound902 line 302
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation903 line 332
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix903 line 338
24. theorem OAI.MUB6.Certificate.PairSemantics.sound903 line 340
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation904 line 370
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix904 line 376
27. theorem OAI.MUB6.Certificate.PairSemantics.sound904 line 378
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation905 line 408
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix905 line 414
30. theorem OAI.MUB6.Certificate.PairSemantics.sound905 line 416
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation906 line 446
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix906 line 452
33. theorem OAI.MUB6.Certificate.PairSemantics.sound906 line 454
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation907 line 484
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix907 line 490
36. theorem OAI.MUB6.Certificate.PairSemantics.sound907 line 492
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation908 line 522
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix908 line 528
39. theorem OAI.MUB6.Certificate.PairSemantics.sound908 line 530
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation909 line 560
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix909 line 566
42. theorem OAI.MUB6.Certificate.PairSemantics.sound909 line 568
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation910 line 598
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix910 line 604
45. theorem OAI.MUB6.Certificate.PairSemantics.sound910 line 606
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation911 line 636
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix911 line 642
48. theorem OAI.MUB6.Certificate.PairSemantics.sound911 line 644
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation912 line 674
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix912 line 680
51. theorem OAI.MUB6.Certificate.PairSemantics.sound912 line 682
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation913 line 713
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix913 line 719
54. theorem OAI.MUB6.Certificate.PairSemantics.sound913 line 721
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation914 line 752
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix914 line 758
57. theorem OAI.MUB6.Certificate.PairSemantics.sound914 line 760
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation915 line 790
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix915 line 796
60. theorem OAI.MUB6.Certificate.PairSemantics.sound915 line 798
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation916 line 828
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix916 line 834
63. theorem OAI.MUB6.Certificate.PairSemantics.sound916 line 836
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation917 line 867
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix917 line 873
66. theorem OAI.MUB6.Certificate.PairSemantics.sound917 line 875
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation918 line 906
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix918 line 912
69. theorem OAI.MUB6.Certificate.PairSemantics.sound918 line 914
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation919 line 945
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix919 line 951
72. theorem OAI.MUB6.Certificate.PairSemantics.sound919 line 953
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation920 line 983
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix920 line 989
75. theorem OAI.MUB6.Certificate.PairSemantics.sound920 line 991
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation921 line 1021
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix921 line 1027
78. theorem OAI.MUB6.Certificate.PairSemantics.sound921 line 1029
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation922 line 1059
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix922 line 1065
81. theorem OAI.MUB6.Certificate.PairSemantics.sound922 line 1067
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation923 line 1097
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix923 line 1103
84. theorem OAI.MUB6.Certificate.PairSemantics.sound923 line 1105
85. theorem OAI.MUB6.Certificate.PairSemantics.sound924 line 1136
86. theorem OAI.MUB6.Certificate.PairSemantics.sound925 line 1141
87. theorem OAI.MUB6.Certificate.PairSemantics.sound926 line 1146
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation927 line 1151
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix927 line 1157
90. theorem OAI.MUB6.Certificate.PairSemantics.sound927 line 1159
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation928 line 1190
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix928 line 1196
93. theorem OAI.MUB6.Certificate.PairSemantics.sound928 line 1198
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation929 line 1229
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix929 line 1235
96. theorem OAI.MUB6.Certificate.PairSemantics.sound929 line 1237
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation930 line 1268
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix930 line 1274
99. theorem OAI.MUB6.Certificate.PairSemantics.sound930 line 1276
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation931 line 1307
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix931 line 1313
102. theorem OAI.MUB6.Certificate.PairSemantics.sound931 line 1315
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation932 line 1346
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix932 line 1352
105. theorem OAI.MUB6.Certificate.PairSemantics.sound932 line 1354
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation933 line 1385
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix933 line 1391
108. theorem OAI.MUB6.Certificate.PairSemantics.sound933 line 1393
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation934 line 1423
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix934 line 1429
111. theorem OAI.MUB6.Certificate.PairSemantics.sound934 line 1431
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation935 line 1461
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix935 line 1467
114. theorem OAI.MUB6.Certificate.PairSemantics.sound935 line 1469
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation936 line 1499
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix936 line 1505
117. theorem OAI.MUB6.Certificate.PairSemantics.sound936 line 1507
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation937 line 1537
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix937 line 1543
120. theorem OAI.MUB6.Certificate.PairSemantics.sound937 line 1545
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation938 line 1575
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix938 line 1581
123. theorem OAI.MUB6.Certificate.PairSemantics.sound938 line 1583
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation939 line 1613
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix939 line 1619
126. theorem OAI.MUB6.Certificate.PairSemantics.sound939 line 1621
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation940 line 1651
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix940 line 1657
129. theorem OAI.MUB6.Certificate.PairSemantics.sound940 line 1659
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation941 line 1689
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix941 line 1695
132. theorem OAI.MUB6.Certificate.PairSemantics.sound941 line 1697
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation942 line 1728
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix942 line 1734
135. theorem OAI.MUB6.Certificate.PairSemantics.sound942 line 1736
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation943 line 1766
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix943 line 1772
138. theorem OAI.MUB6.Certificate.PairSemantics.sound943 line 1774
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation944 line 1805
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix944 line 1811
141. theorem OAI.MUB6.Certificate.PairSemantics.sound944 line 1813
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation945 line 1844
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix945 line 1850
144. theorem OAI.MUB6.Certificate.PairSemantics.sound945 line 1852
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation946 line 1882
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix946 line 1888
147. theorem OAI.MUB6.Certificate.PairSemantics.sound946 line 1890
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation947 line 1920
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix947 line 1926
150. theorem OAI.MUB6.Certificate.PairSemantics.sound947 line 1928
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation948 line 1959
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix948 line 1965
153. theorem OAI.MUB6.Certificate.PairSemantics.sound948 line 1967
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation949 line 1998
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix949 line 2004
156. theorem OAI.MUB6.Certificate.PairSemantics.sound949 line 2006
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation950 line 2036
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix950 line 2042
159. theorem OAI.MUB6.Certificate.PairSemantics.sound950 line 2044
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation951 line 2074
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix951 line 2080
162. theorem OAI.MUB6.Certificate.PairSemantics.sound951 line 2082
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation952 line 2112
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix952 line 2118
165. theorem OAI.MUB6.Certificate.PairSemantics.sound952 line 2120
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation953 line 2150
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix953 line 2156
168. theorem OAI.MUB6.Certificate.PairSemantics.sound953 line 2158
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation954 line 2189
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix954 line 2195
171. theorem OAI.MUB6.Certificate.PairSemantics.sound954 line 2197
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation955 line 2228
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix955 line 2234
174. theorem OAI.MUB6.Certificate.PairSemantics.sound955 line 2236
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation956 line 2267
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix956 line 2273
177. theorem OAI.MUB6.Certificate.PairSemantics.sound956 line 2275
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation957 line 2306
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix957 line 2312
180. theorem OAI.MUB6.Certificate.PairSemantics.sound957 line 2314
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation958 line 2345
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix958 line 2351
183. theorem OAI.MUB6.Certificate.PairSemantics.sound958 line 2353
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation959 line 2384
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix959 line 2390
186. theorem OAI.MUB6.Certificate.PairSemantics.sound959 line 2392