OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound47.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3008 line 75
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3008 line 81
3. theorem OAI.MUB6.Certificate.PairSemantics.sound3008 line 83
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3009 line 123
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3009 line 129
6. theorem OAI.MUB6.Certificate.PairSemantics.sound3009 line 131
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3010 line 171
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3010 line 177
9. theorem OAI.MUB6.Certificate.PairSemantics.sound3010 line 179
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3011 line 219
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3011 line 225
12. theorem OAI.MUB6.Certificate.PairSemantics.sound3011 line 227
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3012 line 267
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3012 line 273
15. theorem OAI.MUB6.Certificate.PairSemantics.sound3012 line 275
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3013 line 315
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3013 line 321
18. theorem OAI.MUB6.Certificate.PairSemantics.sound3013 line 323
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3014 line 363
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3014 line 369
21. theorem OAI.MUB6.Certificate.PairSemantics.sound3014 line 371
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3015 line 411
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3015 line 417
24. theorem OAI.MUB6.Certificate.PairSemantics.sound3015 line 419
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3016 line 459
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3016 line 465
27. theorem OAI.MUB6.Certificate.PairSemantics.sound3016 line 467
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3017 line 507
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3017 line 513
30. theorem OAI.MUB6.Certificate.PairSemantics.sound3017 line 515
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3018 line 555
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3018 line 561
33. theorem OAI.MUB6.Certificate.PairSemantics.sound3018 line 563
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3019 line 603
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3019 line 609
36. theorem OAI.MUB6.Certificate.PairSemantics.sound3019 line 611
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3020 line 651
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3020 line 657
39. theorem OAI.MUB6.Certificate.PairSemantics.sound3020 line 659
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3021 line 699
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3021 line 705
42. theorem OAI.MUB6.Certificate.PairSemantics.sound3021 line 707
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3022 line 747
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3022 line 753
45. theorem OAI.MUB6.Certificate.PairSemantics.sound3022 line 755
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3023 line 795
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3023 line 801
48. theorem OAI.MUB6.Certificate.PairSemantics.sound3023 line 803
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3024 line 843
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3024 line 849
51. theorem OAI.MUB6.Certificate.PairSemantics.sound3024 line 851
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3025 line 891
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3025 line 897
54. theorem OAI.MUB6.Certificate.PairSemantics.sound3025 line 899
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3026 line 939
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3026 line 945
57. theorem OAI.MUB6.Certificate.PairSemantics.sound3026 line 947
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3027 line 987
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3027 line 993
60. theorem OAI.MUB6.Certificate.PairSemantics.sound3027 line 995
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3028 line 1035
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3028 line 1041
63. theorem OAI.MUB6.Certificate.PairSemantics.sound3028 line 1043
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3029 line 1083
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3029 line 1089
66. theorem OAI.MUB6.Certificate.PairSemantics.sound3029 line 1091
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3030 line 1131
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3030 line 1137
69. theorem OAI.MUB6.Certificate.PairSemantics.sound3030 line 1139
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3031 line 1179
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3031 line 1185
72. theorem OAI.MUB6.Certificate.PairSemantics.sound3031 line 1187
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3032 line 1227
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3032 line 1233
75. theorem OAI.MUB6.Certificate.PairSemantics.sound3032 line 1235
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3033 line 1275
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3033 line 1281
78. theorem OAI.MUB6.Certificate.PairSemantics.sound3033 line 1283
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3034 line 1323
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3034 line 1329
81. theorem OAI.MUB6.Certificate.PairSemantics.sound3034 line 1331
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3035 line 1371
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3035 line 1377
84. theorem OAI.MUB6.Certificate.PairSemantics.sound3035 line 1379
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3036 line 1419
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3036 line 1425
87. theorem OAI.MUB6.Certificate.PairSemantics.sound3036 line 1427
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3037 line 1467
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3037 line 1473
90. theorem OAI.MUB6.Certificate.PairSemantics.sound3037 line 1475
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3038 line 1515
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3038 line 1521
93. theorem OAI.MUB6.Certificate.PairSemantics.sound3038 line 1523
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3039 line 1563
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3039 line 1569
96. theorem OAI.MUB6.Certificate.PairSemantics.sound3039 line 1571
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3040 line 1611
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3040 line 1617
99. theorem OAI.MUB6.Certificate.PairSemantics.sound3040 line 1619
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3041 line 1659
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3041 line 1665
102. theorem OAI.MUB6.Certificate.PairSemantics.sound3041 line 1667
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3042 line 1707
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3042 line 1713
105. theorem OAI.MUB6.Certificate.PairSemantics.sound3042 line 1715
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3043 line 1755
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3043 line 1761
108. theorem OAI.MUB6.Certificate.PairSemantics.sound3043 line 1763
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3044 line 1803
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3044 line 1809
111. theorem OAI.MUB6.Certificate.PairSemantics.sound3044 line 1811
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3045 line 1851
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3045 line 1857
114. theorem OAI.MUB6.Certificate.PairSemantics.sound3045 line 1859
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3046 line 1899
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3046 line 1905
117. theorem OAI.MUB6.Certificate.PairSemantics.sound3046 line 1907
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3047 line 1947
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3047 line 1953
120. theorem OAI.MUB6.Certificate.PairSemantics.sound3047 line 1955
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3048 line 1995
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3048 line 2001
123. theorem OAI.MUB6.Certificate.PairSemantics.sound3048 line 2003
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3049 line 2043
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3049 line 2049
126. theorem OAI.MUB6.Certificate.PairSemantics.sound3049 line 2051
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3050 line 2091
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3050 line 2097
129. theorem OAI.MUB6.Certificate.PairSemantics.sound3050 line 2099
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3051 line 2139
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3051 line 2145
132. theorem OAI.MUB6.Certificate.PairSemantics.sound3051 line 2147
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3052 line 2187
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3052 line 2193
135. theorem OAI.MUB6.Certificate.PairSemantics.sound3052 line 2195
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3053 line 2235
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3053 line 2241
138. theorem OAI.MUB6.Certificate.PairSemantics.sound3053 line 2243
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3054 line 2283
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3054 line 2289
141. theorem OAI.MUB6.Certificate.PairSemantics.sound3054 line 2291
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3055 line 2331
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3055 line 2337
144. theorem OAI.MUB6.Certificate.PairSemantics.sound3055 line 2339
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3056 line 2379
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3056 line 2385
147. theorem OAI.MUB6.Certificate.PairSemantics.sound3056 line 2387
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3057 line 2427
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3057 line 2433
150. theorem OAI.MUB6.Certificate.PairSemantics.sound3057 line 2435
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3058 line 2475
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3058 line 2481
153. theorem OAI.MUB6.Certificate.PairSemantics.sound3058 line 2483
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3059 line 2523
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3059 line 2529
156. theorem OAI.MUB6.Certificate.PairSemantics.sound3059 line 2531
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3060 line 2571
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3060 line 2577
159. theorem OAI.MUB6.Certificate.PairSemantics.sound3060 line 2579
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3061 line 2619
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3061 line 2625
162. theorem OAI.MUB6.Certificate.PairSemantics.sound3061 line 2627
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3062 line 2667
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3062 line 2673
165. theorem OAI.MUB6.Certificate.PairSemantics.sound3062 line 2675
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3063 line 2715
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3063 line 2721
168. theorem OAI.MUB6.Certificate.PairSemantics.sound3063 line 2723
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3064 line 2763
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3064 line 2769
171. theorem OAI.MUB6.Certificate.PairSemantics.sound3064 line 2771
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3065 line 2811
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3065 line 2817
174. theorem OAI.MUB6.Certificate.PairSemantics.sound3065 line 2819
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3066 line 2859
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3066 line 2865
177. theorem OAI.MUB6.Certificate.PairSemantics.sound3066 line 2867
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3067 line 2907
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3067 line 2913
180. theorem OAI.MUB6.Certificate.PairSemantics.sound3067 line 2915
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3068 line 2955
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3068 line 2961
183. theorem OAI.MUB6.Certificate.PairSemantics.sound3068 line 2963
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3069 line 3003
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3069 line 3009
186. theorem OAI.MUB6.Certificate.PairSemantics.sound3069 line 3011
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3070 line 3051
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3070 line 3057
189. theorem OAI.MUB6.Certificate.PairSemantics.sound3070 line 3059
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3071 line 3099
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3071 line 3105
192. theorem OAI.MUB6.Certificate.PairSemantics.sound3071 line 3107