OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound49.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3136 line 84
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3136 line 90
3. theorem OAI.MUB6.Certificate.PairSemantics.sound3136 line 92
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3137 line 132
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3137 line 138
6. theorem OAI.MUB6.Certificate.PairSemantics.sound3137 line 140
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3138 line 180
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3138 line 186
9. theorem OAI.MUB6.Certificate.PairSemantics.sound3138 line 188
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3139 line 228
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3139 line 234
12. theorem OAI.MUB6.Certificate.PairSemantics.sound3139 line 236
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3140 line 276
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3140 line 282
15. theorem OAI.MUB6.Certificate.PairSemantics.sound3140 line 284
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3141 line 324
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3141 line 330
18. theorem OAI.MUB6.Certificate.PairSemantics.sound3141 line 332
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3142 line 372
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3142 line 378
21. theorem OAI.MUB6.Certificate.PairSemantics.sound3142 line 380
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3143 line 420
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3143 line 426
24. theorem OAI.MUB6.Certificate.PairSemantics.sound3143 line 428
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3144 line 468
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3144 line 474
27. theorem OAI.MUB6.Certificate.PairSemantics.sound3144 line 476
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3145 line 516
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3145 line 522
30. theorem OAI.MUB6.Certificate.PairSemantics.sound3145 line 524
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3146 line 564
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3146 line 570
33. theorem OAI.MUB6.Certificate.PairSemantics.sound3146 line 572
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3147 line 612
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3147 line 618
36. theorem OAI.MUB6.Certificate.PairSemantics.sound3147 line 620
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3148 line 660
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3148 line 666
39. theorem OAI.MUB6.Certificate.PairSemantics.sound3148 line 668
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3149 line 708
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3149 line 714
42. theorem OAI.MUB6.Certificate.PairSemantics.sound3149 line 716
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3150 line 756
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3150 line 762
45. theorem OAI.MUB6.Certificate.PairSemantics.sound3150 line 764
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3151 line 804
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3151 line 810
48. theorem OAI.MUB6.Certificate.PairSemantics.sound3151 line 812
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3152 line 852
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3152 line 858
51. theorem OAI.MUB6.Certificate.PairSemantics.sound3152 line 860
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3153 line 900
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3153 line 906
54. theorem OAI.MUB6.Certificate.PairSemantics.sound3153 line 908
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3154 line 948
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3154 line 954
57. theorem OAI.MUB6.Certificate.PairSemantics.sound3154 line 956
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3155 line 996
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3155 line 1002
60. theorem OAI.MUB6.Certificate.PairSemantics.sound3155 line 1004
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3156 line 1044
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3156 line 1050
63. theorem OAI.MUB6.Certificate.PairSemantics.sound3156 line 1052
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3157 line 1092
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3157 line 1098
66. theorem OAI.MUB6.Certificate.PairSemantics.sound3157 line 1100
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3158 line 1140
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3158 line 1146
69. theorem OAI.MUB6.Certificate.PairSemantics.sound3158 line 1148
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3159 line 1188
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3159 line 1194
72. theorem OAI.MUB6.Certificate.PairSemantics.sound3159 line 1196
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3160 line 1236
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3160 line 1242
75. theorem OAI.MUB6.Certificate.PairSemantics.sound3160 line 1244
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3161 line 1284
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3161 line 1290
78. theorem OAI.MUB6.Certificate.PairSemantics.sound3161 line 1292
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3162 line 1332
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3162 line 1338
81. theorem OAI.MUB6.Certificate.PairSemantics.sound3162 line 1340
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3163 line 1380
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3163 line 1386
84. theorem OAI.MUB6.Certificate.PairSemantics.sound3163 line 1388
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3164 line 1428
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3164 line 1434
87. theorem OAI.MUB6.Certificate.PairSemantics.sound3164 line 1436
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3165 line 1476
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3165 line 1482
90. theorem OAI.MUB6.Certificate.PairSemantics.sound3165 line 1484
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3166 line 1524
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3166 line 1530
93. theorem OAI.MUB6.Certificate.PairSemantics.sound3166 line 1532
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3167 line 1572
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3167 line 1578
96. theorem OAI.MUB6.Certificate.PairSemantics.sound3167 line 1580
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3168 line 1620
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3168 line 1626
99. theorem OAI.MUB6.Certificate.PairSemantics.sound3168 line 1628
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3169 line 1668
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3169 line 1674
102. theorem OAI.MUB6.Certificate.PairSemantics.sound3169 line 1676
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3170 line 1716
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3170 line 1722
105. theorem OAI.MUB6.Certificate.PairSemantics.sound3170 line 1724
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3171 line 1764
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3171 line 1770
108. theorem OAI.MUB6.Certificate.PairSemantics.sound3171 line 1772
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3172 line 1812
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3172 line 1818
111. theorem OAI.MUB6.Certificate.PairSemantics.sound3172 line 1820
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3173 line 1860
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3173 line 1866
114. theorem OAI.MUB6.Certificate.PairSemantics.sound3173 line 1868
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3174 line 1908
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3174 line 1914
117. theorem OAI.MUB6.Certificate.PairSemantics.sound3174 line 1916
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3175 line 1956
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3175 line 1962
120. theorem OAI.MUB6.Certificate.PairSemantics.sound3175 line 1964
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3176 line 2004
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3176 line 2010
123. theorem OAI.MUB6.Certificate.PairSemantics.sound3176 line 2012
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3177 line 2052
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3177 line 2058
126. theorem OAI.MUB6.Certificate.PairSemantics.sound3177 line 2060
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3178 line 2100
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3178 line 2106
129. theorem OAI.MUB6.Certificate.PairSemantics.sound3178 line 2108
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3179 line 2148
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3179 line 2154
132. theorem OAI.MUB6.Certificate.PairSemantics.sound3179 line 2156
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3180 line 2196
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3180 line 2202
135. theorem OAI.MUB6.Certificate.PairSemantics.sound3180 line 2204
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3181 line 2244
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3181 line 2250
138. theorem OAI.MUB6.Certificate.PairSemantics.sound3181 line 2252
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3182 line 2292
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3182 line 2298
141. theorem OAI.MUB6.Certificate.PairSemantics.sound3182 line 2300
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3183 line 2340
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3183 line 2346
144. theorem OAI.MUB6.Certificate.PairSemantics.sound3183 line 2348
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3184 line 2388
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3184 line 2394
147. theorem OAI.MUB6.Certificate.PairSemantics.sound3184 line 2396
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3185 line 2436
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3185 line 2442
150. theorem OAI.MUB6.Certificate.PairSemantics.sound3185 line 2444
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3186 line 2484
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3186 line 2490
153. theorem OAI.MUB6.Certificate.PairSemantics.sound3186 line 2492
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3187 line 2532
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3187 line 2538
156. theorem OAI.MUB6.Certificate.PairSemantics.sound3187 line 2540
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3188 line 2580
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3188 line 2586
159. theorem OAI.MUB6.Certificate.PairSemantics.sound3188 line 2588
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3189 line 2628
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3189 line 2634
162. theorem OAI.MUB6.Certificate.PairSemantics.sound3189 line 2636
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3190 line 2676
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3190 line 2682
165. theorem OAI.MUB6.Certificate.PairSemantics.sound3190 line 2684
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3191 line 2724
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3191 line 2730
168. theorem OAI.MUB6.Certificate.PairSemantics.sound3191 line 2732
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3192 line 2772
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3192 line 2778
171. theorem OAI.MUB6.Certificate.PairSemantics.sound3192 line 2780
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3193 line 2820
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3193 line 2826
174. theorem OAI.MUB6.Certificate.PairSemantics.sound3193 line 2828
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3194 line 2868
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3194 line 2874
177. theorem OAI.MUB6.Certificate.PairSemantics.sound3194 line 2876
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3195 line 2916
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3195 line 2922
180. theorem OAI.MUB6.Certificate.PairSemantics.sound3195 line 2924
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3196 line 2964
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3196 line 2970
183. theorem OAI.MUB6.Certificate.PairSemantics.sound3196 line 2972
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3197 line 3012
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3197 line 3018
186. theorem OAI.MUB6.Certificate.PairSemantics.sound3197 line 3020
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3198 line 3060
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3198 line 3066
189. theorem OAI.MUB6.Certificate.PairSemantics.sound3198 line 3068
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation3199 line 3108
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix3199 line 3114
192. theorem OAI.MUB6.Certificate.PairSemantics.sound3199 line 3116