OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound48.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3072 line 95
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3072 line 101
3. theorem OAI.MUB6.Certificate.PairSemantics.sound3072 line 103
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3073 line 143
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3073 line 149
6. theorem OAI.MUB6.Certificate.PairSemantics.sound3073 line 151
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3074 line 191
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3074 line 197
9. theorem OAI.MUB6.Certificate.PairSemantics.sound3074 line 199
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3075 line 239
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3075 line 245
12. theorem OAI.MUB6.Certificate.PairSemantics.sound3075 line 247
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3076 line 287
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3076 line 293
15. theorem OAI.MUB6.Certificate.PairSemantics.sound3076 line 295
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3077 line 335
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3077 line 341
18. theorem OAI.MUB6.Certificate.PairSemantics.sound3077 line 343
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3078 line 383
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3078 line 389
21. theorem OAI.MUB6.Certificate.PairSemantics.sound3078 line 391
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3079 line 431
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3079 line 437
24. theorem OAI.MUB6.Certificate.PairSemantics.sound3079 line 439
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3080 line 479
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3080 line 485
27. theorem OAI.MUB6.Certificate.PairSemantics.sound3080 line 487
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3081 line 527
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3081 line 533
30. theorem OAI.MUB6.Certificate.PairSemantics.sound3081 line 535
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3082 line 575
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3082 line 581
33. theorem OAI.MUB6.Certificate.PairSemantics.sound3082 line 583
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3083 line 623
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3083 line 629
36. theorem OAI.MUB6.Certificate.PairSemantics.sound3083 line 631
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3084 line 671
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3084 line 677
39. theorem OAI.MUB6.Certificate.PairSemantics.sound3084 line 679
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3085 line 719
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3085 line 725
42. theorem OAI.MUB6.Certificate.PairSemantics.sound3085 line 727
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3086 line 767
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3086 line 773
45. theorem OAI.MUB6.Certificate.PairSemantics.sound3086 line 775
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3087 line 815
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3087 line 821
48. theorem OAI.MUB6.Certificate.PairSemantics.sound3087 line 823
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3088 line 863
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3088 line 869
51. theorem OAI.MUB6.Certificate.PairSemantics.sound3088 line 871
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3089 line 911
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3089 line 917
54. theorem OAI.MUB6.Certificate.PairSemantics.sound3089 line 919
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3090 line 959
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3090 line 965
57. theorem OAI.MUB6.Certificate.PairSemantics.sound3090 line 967
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3091 line 1007
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3091 line 1013
60. theorem OAI.MUB6.Certificate.PairSemantics.sound3091 line 1015
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3092 line 1055
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3092 line 1061
63. theorem OAI.MUB6.Certificate.PairSemantics.sound3092 line 1063
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3093 line 1103
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3093 line 1109
66. theorem OAI.MUB6.Certificate.PairSemantics.sound3093 line 1111
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3094 line 1151
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3094 line 1157
69. theorem OAI.MUB6.Certificate.PairSemantics.sound3094 line 1159
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3095 line 1199
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3095 line 1205
72. theorem OAI.MUB6.Certificate.PairSemantics.sound3095 line 1207
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3096 line 1247
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3096 line 1253
75. theorem OAI.MUB6.Certificate.PairSemantics.sound3096 line 1255
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3097 line 1295
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3097 line 1301
78. theorem OAI.MUB6.Certificate.PairSemantics.sound3097 line 1303
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3098 line 1343
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3098 line 1349
81. theorem OAI.MUB6.Certificate.PairSemantics.sound3098 line 1351
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3099 line 1391
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3099 line 1397
84. theorem OAI.MUB6.Certificate.PairSemantics.sound3099 line 1399
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3100 line 1439
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3100 line 1445
87. theorem OAI.MUB6.Certificate.PairSemantics.sound3100 line 1447
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3101 line 1487
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3101 line 1493
90. theorem OAI.MUB6.Certificate.PairSemantics.sound3101 line 1495
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3102 line 1535
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3102 line 1541
93. theorem OAI.MUB6.Certificate.PairSemantics.sound3102 line 1543
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3103 line 1583
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3103 line 1589
96. theorem OAI.MUB6.Certificate.PairSemantics.sound3103 line 1591
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3104 line 1631
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3104 line 1637
99. theorem OAI.MUB6.Certificate.PairSemantics.sound3104 line 1639
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3105 line 1679
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3105 line 1685
102. theorem OAI.MUB6.Certificate.PairSemantics.sound3105 line 1687
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3106 line 1727
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3106 line 1733
105. theorem OAI.MUB6.Certificate.PairSemantics.sound3106 line 1735
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3107 line 1775
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3107 line 1781
108. theorem OAI.MUB6.Certificate.PairSemantics.sound3107 line 1783
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3108 line 1823
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3108 line 1829
111. theorem OAI.MUB6.Certificate.PairSemantics.sound3108 line 1831
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3109 line 1871
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3109 line 1877
114. theorem OAI.MUB6.Certificate.PairSemantics.sound3109 line 1879
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3110 line 1919
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3110 line 1925
117. theorem OAI.MUB6.Certificate.PairSemantics.sound3110 line 1927
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3111 line 1967
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3111 line 1973
120. theorem OAI.MUB6.Certificate.PairSemantics.sound3111 line 1975
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3112 line 2015
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3112 line 2021
123. theorem OAI.MUB6.Certificate.PairSemantics.sound3112 line 2023
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3113 line 2063
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3113 line 2069
126. theorem OAI.MUB6.Certificate.PairSemantics.sound3113 line 2071
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3114 line 2111
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3114 line 2117
129. theorem OAI.MUB6.Certificate.PairSemantics.sound3114 line 2119
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3115 line 2159
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3115 line 2165
132. theorem OAI.MUB6.Certificate.PairSemantics.sound3115 line 2167
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3116 line 2207
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3116 line 2213
135. theorem OAI.MUB6.Certificate.PairSemantics.sound3116 line 2215
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3117 line 2255
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3117 line 2261
138. theorem OAI.MUB6.Certificate.PairSemantics.sound3117 line 2263
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3118 line 2303
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3118 line 2309
141. theorem OAI.MUB6.Certificate.PairSemantics.sound3118 line 2311
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3119 line 2351
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3119 line 2357
144. theorem OAI.MUB6.Certificate.PairSemantics.sound3119 line 2359
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3120 line 2399
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3120 line 2405
147. theorem OAI.MUB6.Certificate.PairSemantics.sound3120 line 2407
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3121 line 2447
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3121 line 2453
150. theorem OAI.MUB6.Certificate.PairSemantics.sound3121 line 2455
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3122 line 2495
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3122 line 2501
153. theorem OAI.MUB6.Certificate.PairSemantics.sound3122 line 2503
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3123 line 2543
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3123 line 2549
156. theorem OAI.MUB6.Certificate.PairSemantics.sound3123 line 2551
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3124 line 2591
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3124 line 2597
159. theorem OAI.MUB6.Certificate.PairSemantics.sound3124 line 2599
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3125 line 2639
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3125 line 2645
162. theorem OAI.MUB6.Certificate.PairSemantics.sound3125 line 2647
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3126 line 2687
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3126 line 2693
165. theorem OAI.MUB6.Certificate.PairSemantics.sound3126 line 2695
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3127 line 2735
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3127 line 2741
168. theorem OAI.MUB6.Certificate.PairSemantics.sound3127 line 2743
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3128 line 2783
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3128 line 2789
171. theorem OAI.MUB6.Certificate.PairSemantics.sound3128 line 2791
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3129 line 2831
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3129 line 2837
174. theorem OAI.MUB6.Certificate.PairSemantics.sound3129 line 2839
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3130 line 2879
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3130 line 2885
177. theorem OAI.MUB6.Certificate.PairSemantics.sound3130 line 2887
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3131 line 2927
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3131 line 2933
180. theorem OAI.MUB6.Certificate.PairSemantics.sound3131 line 2935
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3132 line 2975
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3132 line 2981
183. theorem OAI.MUB6.Certificate.PairSemantics.sound3132 line 2983
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3133 line 3023
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3133 line 3029
186. theorem OAI.MUB6.Certificate.PairSemantics.sound3133 line 3031
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3134 line 3071
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3134 line 3077
189. theorem OAI.MUB6.Certificate.PairSemantics.sound3134 line 3079
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3135 line 3119
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3135 line 3125
192. theorem OAI.MUB6.Certificate.PairSemantics.sound3135 line 3127