OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound46.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2944 line 84
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2944 line 90
3. theorem OAI.MUB6.Certificate.PairSemantics.sound2944 line 92
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2945 line 132
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2945 line 138
6. theorem OAI.MUB6.Certificate.PairSemantics.sound2945 line 140
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2946 line 180
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2946 line 186
9. theorem OAI.MUB6.Certificate.PairSemantics.sound2946 line 188
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2947 line 228
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2947 line 234
12. theorem OAI.MUB6.Certificate.PairSemantics.sound2947 line 236
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2948 line 276
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2948 line 282
15. theorem OAI.MUB6.Certificate.PairSemantics.sound2948 line 284
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2949 line 324
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2949 line 330
18. theorem OAI.MUB6.Certificate.PairSemantics.sound2949 line 332
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2950 line 372
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2950 line 378
21. theorem OAI.MUB6.Certificate.PairSemantics.sound2950 line 380
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2951 line 420
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2951 line 426
24. theorem OAI.MUB6.Certificate.PairSemantics.sound2951 line 428
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2952 line 468
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2952 line 474
27. theorem OAI.MUB6.Certificate.PairSemantics.sound2952 line 476
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2953 line 516
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2953 line 522
30. theorem OAI.MUB6.Certificate.PairSemantics.sound2953 line 524
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2954 line 564
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2954 line 570
33. theorem OAI.MUB6.Certificate.PairSemantics.sound2954 line 572
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2955 line 612
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2955 line 618
36. theorem OAI.MUB6.Certificate.PairSemantics.sound2955 line 620
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2956 line 660
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2956 line 666
39. theorem OAI.MUB6.Certificate.PairSemantics.sound2956 line 668
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2957 line 708
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2957 line 714
42. theorem OAI.MUB6.Certificate.PairSemantics.sound2957 line 716
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2958 line 756
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2958 line 762
45. theorem OAI.MUB6.Certificate.PairSemantics.sound2958 line 764
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2959 line 804
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2959 line 810
48. theorem OAI.MUB6.Certificate.PairSemantics.sound2959 line 812
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2960 line 852
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2960 line 858
51. theorem OAI.MUB6.Certificate.PairSemantics.sound2960 line 860
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2961 line 900
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2961 line 906
54. theorem OAI.MUB6.Certificate.PairSemantics.sound2961 line 908
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2962 line 948
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2962 line 954
57. theorem OAI.MUB6.Certificate.PairSemantics.sound2962 line 956
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2963 line 996
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2963 line 1002
60. theorem OAI.MUB6.Certificate.PairSemantics.sound2963 line 1004
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2964 line 1044
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2964 line 1050
63. theorem OAI.MUB6.Certificate.PairSemantics.sound2964 line 1052
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2965 line 1092
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2965 line 1098
66. theorem OAI.MUB6.Certificate.PairSemantics.sound2965 line 1100
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2966 line 1140
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2966 line 1146
69. theorem OAI.MUB6.Certificate.PairSemantics.sound2966 line 1148
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2967 line 1188
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2967 line 1194
72. theorem OAI.MUB6.Certificate.PairSemantics.sound2967 line 1196
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2968 line 1236
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2968 line 1242
75. theorem OAI.MUB6.Certificate.PairSemantics.sound2968 line 1244
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2969 line 1284
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2969 line 1290
78. theorem OAI.MUB6.Certificate.PairSemantics.sound2969 line 1292
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2970 line 1332
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2970 line 1338
81. theorem OAI.MUB6.Certificate.PairSemantics.sound2970 line 1340
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2971 line 1380
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2971 line 1386
84. theorem OAI.MUB6.Certificate.PairSemantics.sound2971 line 1388
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2972 line 1428
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2972 line 1434
87. theorem OAI.MUB6.Certificate.PairSemantics.sound2972 line 1436
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2973 line 1476
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2973 line 1482
90. theorem OAI.MUB6.Certificate.PairSemantics.sound2973 line 1484
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2974 line 1524
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2974 line 1530
93. theorem OAI.MUB6.Certificate.PairSemantics.sound2974 line 1532
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2975 line 1572
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2975 line 1578
96. theorem OAI.MUB6.Certificate.PairSemantics.sound2975 line 1580
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2976 line 1620
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2976 line 1626
99. theorem OAI.MUB6.Certificate.PairSemantics.sound2976 line 1628
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2977 line 1668
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2977 line 1674
102. theorem OAI.MUB6.Certificate.PairSemantics.sound2977 line 1676
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2978 line 1716
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2978 line 1722
105. theorem OAI.MUB6.Certificate.PairSemantics.sound2978 line 1724
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2979 line 1764
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2979 line 1770
108. theorem OAI.MUB6.Certificate.PairSemantics.sound2979 line 1772
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2980 line 1812
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2980 line 1818
111. theorem OAI.MUB6.Certificate.PairSemantics.sound2980 line 1820
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2981 line 1860
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2981 line 1866
114. theorem OAI.MUB6.Certificate.PairSemantics.sound2981 line 1868
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2982 line 1908
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2982 line 1914
117. theorem OAI.MUB6.Certificate.PairSemantics.sound2982 line 1916
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2983 line 1956
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2983 line 1962
120. theorem OAI.MUB6.Certificate.PairSemantics.sound2983 line 1964
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2984 line 2004
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2984 line 2010
123. theorem OAI.MUB6.Certificate.PairSemantics.sound2984 line 2012
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2985 line 2052
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2985 line 2058
126. theorem OAI.MUB6.Certificate.PairSemantics.sound2985 line 2060
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2986 line 2100
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2986 line 2106
129. theorem OAI.MUB6.Certificate.PairSemantics.sound2986 line 2108
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2987 line 2148
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2987 line 2154
132. theorem OAI.MUB6.Certificate.PairSemantics.sound2987 line 2156
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2988 line 2196
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2988 line 2202
135. theorem OAI.MUB6.Certificate.PairSemantics.sound2988 line 2204
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2989 line 2244
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2989 line 2250
138. theorem OAI.MUB6.Certificate.PairSemantics.sound2989 line 2252
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2990 line 2292
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2990 line 2298
141. theorem OAI.MUB6.Certificate.PairSemantics.sound2990 line 2300
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2991 line 2340
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2991 line 2346
144. theorem OAI.MUB6.Certificate.PairSemantics.sound2991 line 2348
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2992 line 2388
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2992 line 2394
147. theorem OAI.MUB6.Certificate.PairSemantics.sound2992 line 2396
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2993 line 2436
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2993 line 2442
150. theorem OAI.MUB6.Certificate.PairSemantics.sound2993 line 2444
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2994 line 2484
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2994 line 2490
153. theorem OAI.MUB6.Certificate.PairSemantics.sound2994 line 2492
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2995 line 2532
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2995 line 2538
156. theorem OAI.MUB6.Certificate.PairSemantics.sound2995 line 2540
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2996 line 2580
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2996 line 2586
159. theorem OAI.MUB6.Certificate.PairSemantics.sound2996 line 2588
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2997 line 2628
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2997 line 2634
162. theorem OAI.MUB6.Certificate.PairSemantics.sound2997 line 2636
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2998 line 2676
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2998 line 2682
165. theorem OAI.MUB6.Certificate.PairSemantics.sound2998 line 2684
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2999 line 2724
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2999 line 2730
168. theorem OAI.MUB6.Certificate.PairSemantics.sound2999 line 2732
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3000 line 2772
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3000 line 2778
171. theorem OAI.MUB6.Certificate.PairSemantics.sound3000 line 2780
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3001 line 2820
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3001 line 2826
174. theorem OAI.MUB6.Certificate.PairSemantics.sound3001 line 2828
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3002 line 2868
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3002 line 2874
177. theorem OAI.MUB6.Certificate.PairSemantics.sound3002 line 2876
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3003 line 2916
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3003 line 2922
180. theorem OAI.MUB6.Certificate.PairSemantics.sound3003 line 2924
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3004 line 2964
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3004 line 2970
183. theorem OAI.MUB6.Certificate.PairSemantics.sound3004 line 2972
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3005 line 3012
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3005 line 3018
186. theorem OAI.MUB6.Certificate.PairSemantics.sound3005 line 3020
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3006 line 3060
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3006 line 3066
189. theorem OAI.MUB6.Certificate.PairSemantics.sound3006 line 3068
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3007 line 3108
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3007 line 3114
192. theorem OAI.MUB6.Certificate.PairSemantics.sound3007 line 3116