OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound45.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2880 line 81
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2880 line 87
3. theorem OAI.MUB6.Certificate.PairSemantics.sound2880 line 89
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2881 line 129
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2881 line 135
6. theorem OAI.MUB6.Certificate.PairSemantics.sound2881 line 137
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2882 line 177
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2882 line 183
9. theorem OAI.MUB6.Certificate.PairSemantics.sound2882 line 185
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2883 line 225
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2883 line 231
12. theorem OAI.MUB6.Certificate.PairSemantics.sound2883 line 233
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2884 line 273
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2884 line 279
15. theorem OAI.MUB6.Certificate.PairSemantics.sound2884 line 281
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2885 line 321
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2885 line 327
18. theorem OAI.MUB6.Certificate.PairSemantics.sound2885 line 329
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2886 line 369
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2886 line 375
21. theorem OAI.MUB6.Certificate.PairSemantics.sound2886 line 377
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2887 line 417
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2887 line 423
24. theorem OAI.MUB6.Certificate.PairSemantics.sound2887 line 425
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2888 line 465
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2888 line 471
27. theorem OAI.MUB6.Certificate.PairSemantics.sound2888 line 473
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2889 line 513
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2889 line 519
30. theorem OAI.MUB6.Certificate.PairSemantics.sound2889 line 521
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2890 line 561
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2890 line 567
33. theorem OAI.MUB6.Certificate.PairSemantics.sound2890 line 569
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2891 line 609
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2891 line 615
36. theorem OAI.MUB6.Certificate.PairSemantics.sound2891 line 617
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2892 line 657
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2892 line 663
39. theorem OAI.MUB6.Certificate.PairSemantics.sound2892 line 665
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2893 line 705
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2893 line 711
42. theorem OAI.MUB6.Certificate.PairSemantics.sound2893 line 713
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2894 line 753
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2894 line 759
45. theorem OAI.MUB6.Certificate.PairSemantics.sound2894 line 761
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2895 line 801
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2895 line 807
48. theorem OAI.MUB6.Certificate.PairSemantics.sound2895 line 809
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2896 line 849
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2896 line 855
51. theorem OAI.MUB6.Certificate.PairSemantics.sound2896 line 857
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2897 line 897
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2897 line 903
54. theorem OAI.MUB6.Certificate.PairSemantics.sound2897 line 905
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2898 line 945
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2898 line 951
57. theorem OAI.MUB6.Certificate.PairSemantics.sound2898 line 953
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2899 line 993
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2899 line 999
60. theorem OAI.MUB6.Certificate.PairSemantics.sound2899 line 1001
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2900 line 1041
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2900 line 1047
63. theorem OAI.MUB6.Certificate.PairSemantics.sound2900 line 1049
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2901 line 1089
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2901 line 1095
66. theorem OAI.MUB6.Certificate.PairSemantics.sound2901 line 1097
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2902 line 1137
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2902 line 1143
69. theorem OAI.MUB6.Certificate.PairSemantics.sound2902 line 1145
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2903 line 1185
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2903 line 1191
72. theorem OAI.MUB6.Certificate.PairSemantics.sound2903 line 1193
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2904 line 1233
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2904 line 1239
75. theorem OAI.MUB6.Certificate.PairSemantics.sound2904 line 1241
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2905 line 1281
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2905 line 1287
78. theorem OAI.MUB6.Certificate.PairSemantics.sound2905 line 1289
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2906 line 1329
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2906 line 1335
81. theorem OAI.MUB6.Certificate.PairSemantics.sound2906 line 1337
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2907 line 1377
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2907 line 1383
84. theorem OAI.MUB6.Certificate.PairSemantics.sound2907 line 1385
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2908 line 1425
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2908 line 1431
87. theorem OAI.MUB6.Certificate.PairSemantics.sound2908 line 1433
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2909 line 1473
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2909 line 1479
90. theorem OAI.MUB6.Certificate.PairSemantics.sound2909 line 1481
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2910 line 1521
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2910 line 1527
93. theorem OAI.MUB6.Certificate.PairSemantics.sound2910 line 1529
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2911 line 1569
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2911 line 1575
96. theorem OAI.MUB6.Certificate.PairSemantics.sound2911 line 1577
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2912 line 1617
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2912 line 1623
99. theorem OAI.MUB6.Certificate.PairSemantics.sound2912 line 1625
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2913 line 1665
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2913 line 1671
102. theorem OAI.MUB6.Certificate.PairSemantics.sound2913 line 1673
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2914 line 1713
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2914 line 1719
105. theorem OAI.MUB6.Certificate.PairSemantics.sound2914 line 1721
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2915 line 1761
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2915 line 1767
108. theorem OAI.MUB6.Certificate.PairSemantics.sound2915 line 1769
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2916 line 1809
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2916 line 1815
111. theorem OAI.MUB6.Certificate.PairSemantics.sound2916 line 1817
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2917 line 1857
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2917 line 1863
114. theorem OAI.MUB6.Certificate.PairSemantics.sound2917 line 1865
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2918 line 1905
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2918 line 1911
117. theorem OAI.MUB6.Certificate.PairSemantics.sound2918 line 1913
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2919 line 1953
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2919 line 1959
120. theorem OAI.MUB6.Certificate.PairSemantics.sound2919 line 1961
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2920 line 2001
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2920 line 2007
123. theorem OAI.MUB6.Certificate.PairSemantics.sound2920 line 2009
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2921 line 2049
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2921 line 2055
126. theorem OAI.MUB6.Certificate.PairSemantics.sound2921 line 2057
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2922 line 2097
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2922 line 2103
129. theorem OAI.MUB6.Certificate.PairSemantics.sound2922 line 2105
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2923 line 2145
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2923 line 2151
132. theorem OAI.MUB6.Certificate.PairSemantics.sound2923 line 2153
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2924 line 2193
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2924 line 2199
135. theorem OAI.MUB6.Certificate.PairSemantics.sound2924 line 2201
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2925 line 2241
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2925 line 2247
138. theorem OAI.MUB6.Certificate.PairSemantics.sound2925 line 2249
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2926 line 2289
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2926 line 2295
141. theorem OAI.MUB6.Certificate.PairSemantics.sound2926 line 2297
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2927 line 2337
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2927 line 2343
144. theorem OAI.MUB6.Certificate.PairSemantics.sound2927 line 2345
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2928 line 2385
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2928 line 2391
147. theorem OAI.MUB6.Certificate.PairSemantics.sound2928 line 2393
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2929 line 2433
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2929 line 2439
150. theorem OAI.MUB6.Certificate.PairSemantics.sound2929 line 2441
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2930 line 2481
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2930 line 2487
153. theorem OAI.MUB6.Certificate.PairSemantics.sound2930 line 2489
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2931 line 2529
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2931 line 2535
156. theorem OAI.MUB6.Certificate.PairSemantics.sound2931 line 2537
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2932 line 2577
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2932 line 2583
159. theorem OAI.MUB6.Certificate.PairSemantics.sound2932 line 2585
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2933 line 2625
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2933 line 2631
162. theorem OAI.MUB6.Certificate.PairSemantics.sound2933 line 2633
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2934 line 2673
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2934 line 2679
165. theorem OAI.MUB6.Certificate.PairSemantics.sound2934 line 2681
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2935 line 2721
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2935 line 2727
168. theorem OAI.MUB6.Certificate.PairSemantics.sound2935 line 2729
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2936 line 2769
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2936 line 2775
171. theorem OAI.MUB6.Certificate.PairSemantics.sound2936 line 2777
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2937 line 2817
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2937 line 2823
174. theorem OAI.MUB6.Certificate.PairSemantics.sound2937 line 2825
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2938 line 2865
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2938 line 2871
177. theorem OAI.MUB6.Certificate.PairSemantics.sound2938 line 2873
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2939 line 2913
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2939 line 2919
180. theorem OAI.MUB6.Certificate.PairSemantics.sound2939 line 2921
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2940 line 2961
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2940 line 2967
183. theorem OAI.MUB6.Certificate.PairSemantics.sound2940 line 2969
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2941 line 3009
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2941 line 3015
186. theorem OAI.MUB6.Certificate.PairSemantics.sound2941 line 3017
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2942 line 3057
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2942 line 3063
189. theorem OAI.MUB6.Certificate.PairSemantics.sound2942 line 3065
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2943 line 3105
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2943 line 3111
192. theorem OAI.MUB6.Certificate.PairSemantics.sound2943 line 3113