OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound12.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation768 line 57
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix768 line 63
3. theorem OAI.MUB6.Certificate.PairSemantics.sound768 line 65
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation769 line 95
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix769 line 101
6. theorem OAI.MUB6.Certificate.PairSemantics.sound769 line 103
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation770 line 133
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix770 line 139
9. theorem OAI.MUB6.Certificate.PairSemantics.sound770 line 141
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation771 line 172
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix771 line 178
12. theorem OAI.MUB6.Certificate.PairSemantics.sound771 line 180
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation772 line 210
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix772 line 216
15. theorem OAI.MUB6.Certificate.PairSemantics.sound772 line 218
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation773 line 249
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix773 line 255
18. theorem OAI.MUB6.Certificate.PairSemantics.sound773 line 257
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation774 line 288
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix774 line 294
21. theorem OAI.MUB6.Certificate.PairSemantics.sound774 line 296
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation775 line 326
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix775 line 332
24. theorem OAI.MUB6.Certificate.PairSemantics.sound775 line 334
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation776 line 364
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix776 line 370
27. theorem OAI.MUB6.Certificate.PairSemantics.sound776 line 372
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation777 line 403
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix777 line 409
30. theorem OAI.MUB6.Certificate.PairSemantics.sound777 line 411
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation778 line 442
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix778 line 448
33. theorem OAI.MUB6.Certificate.PairSemantics.sound778 line 450
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation779 line 481
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix779 line 487
36. theorem OAI.MUB6.Certificate.PairSemantics.sound779 line 489
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation780 line 519
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix780 line 525
39. theorem OAI.MUB6.Certificate.PairSemantics.sound780 line 527
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation781 line 557
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix781 line 563
42. theorem OAI.MUB6.Certificate.PairSemantics.sound781 line 565
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation782 line 595
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix782 line 601
45. theorem OAI.MUB6.Certificate.PairSemantics.sound782 line 603
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation783 line 633
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix783 line 639
48. theorem OAI.MUB6.Certificate.PairSemantics.sound783 line 641
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation784 line 672
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix784 line 678
51. theorem OAI.MUB6.Certificate.PairSemantics.sound784 line 680
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation785 line 711
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix785 line 717
54. theorem OAI.MUB6.Certificate.PairSemantics.sound785 line 719
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation786 line 750
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix786 line 756
57. theorem OAI.MUB6.Certificate.PairSemantics.sound786 line 758
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation787 line 788
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix787 line 794
60. theorem OAI.MUB6.Certificate.PairSemantics.sound787 line 796
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation788 line 826
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix788 line 832
63. theorem OAI.MUB6.Certificate.PairSemantics.sound788 line 834
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation789 line 865
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix789 line 871
66. theorem OAI.MUB6.Certificate.PairSemantics.sound789 line 873
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation790 line 904
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix790 line 910
69. theorem OAI.MUB6.Certificate.PairSemantics.sound790 line 912
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation791 line 943
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix791 line 949
72. theorem OAI.MUB6.Certificate.PairSemantics.sound791 line 951
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation792 line 982
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix792 line 988
75. theorem OAI.MUB6.Certificate.PairSemantics.sound792 line 990
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation793 line 1021
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix793 line 1027
78. theorem OAI.MUB6.Certificate.PairSemantics.sound793 line 1029
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation794 line 1060
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix794 line 1066
81. theorem OAI.MUB6.Certificate.PairSemantics.sound794 line 1068
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation795 line 1099
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix795 line 1105
84. theorem OAI.MUB6.Certificate.PairSemantics.sound795 line 1107
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation796 line 1137
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix796 line 1143
87. theorem OAI.MUB6.Certificate.PairSemantics.sound796 line 1145
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation797 line 1175
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix797 line 1181
90. theorem OAI.MUB6.Certificate.PairSemantics.sound797 line 1183
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation798 line 1213
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix798 line 1219
93. theorem OAI.MUB6.Certificate.PairSemantics.sound798 line 1221
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation799 line 1251
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix799 line 1257
96. theorem OAI.MUB6.Certificate.PairSemantics.sound799 line 1259
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation800 line 1289
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix800 line 1295
99. theorem OAI.MUB6.Certificate.PairSemantics.sound800 line 1297
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation801 line 1327
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix801 line 1333
102. theorem OAI.MUB6.Certificate.PairSemantics.sound801 line 1335
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation802 line 1365
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix802 line 1371
105. theorem OAI.MUB6.Certificate.PairSemantics.sound802 line 1373
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation803 line 1403
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix803 line 1409
108. theorem OAI.MUB6.Certificate.PairSemantics.sound803 line 1411
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation804 line 1441
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix804 line 1447
111. theorem OAI.MUB6.Certificate.PairSemantics.sound804 line 1449
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation805 line 1480
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix805 line 1486
114. theorem OAI.MUB6.Certificate.PairSemantics.sound805 line 1488
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation806 line 1518
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix806 line 1524
117. theorem OAI.MUB6.Certificate.PairSemantics.sound806 line 1526
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation807 line 1556
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix807 line 1562
120. theorem OAI.MUB6.Certificate.PairSemantics.sound807 line 1564
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation808 line 1594
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix808 line 1600
123. theorem OAI.MUB6.Certificate.PairSemantics.sound808 line 1602
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation809 line 1633
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix809 line 1639
126. theorem OAI.MUB6.Certificate.PairSemantics.sound809 line 1641
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation810 line 1672
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix810 line 1678
129. theorem OAI.MUB6.Certificate.PairSemantics.sound810 line 1680
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation811 line 1710
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix811 line 1716
132. theorem OAI.MUB6.Certificate.PairSemantics.sound811 line 1718
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation812 line 1748
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix812 line 1754
135. theorem OAI.MUB6.Certificate.PairSemantics.sound812 line 1756
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation813 line 1787
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix813 line 1793
138. theorem OAI.MUB6.Certificate.PairSemantics.sound813 line 1795
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation814 line 1826
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix814 line 1832
141. theorem OAI.MUB6.Certificate.PairSemantics.sound814 line 1834
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation815 line 1865
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix815 line 1871
144. theorem OAI.MUB6.Certificate.PairSemantics.sound815 line 1873
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation816 line 1904
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix816 line 1910
147. theorem OAI.MUB6.Certificate.PairSemantics.sound816 line 1912
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation817 line 1942
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix817 line 1948
150. theorem OAI.MUB6.Certificate.PairSemantics.sound817 line 1950
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation818 line 1980
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix818 line 1986
153. theorem OAI.MUB6.Certificate.PairSemantics.sound818 line 1988
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation819 line 2018
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix819 line 2024
156. theorem OAI.MUB6.Certificate.PairSemantics.sound819 line 2026
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation820 line 2056
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix820 line 2062
159. theorem OAI.MUB6.Certificate.PairSemantics.sound820 line 2064
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation821 line 2095
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix821 line 2101
162. theorem OAI.MUB6.Certificate.PairSemantics.sound821 line 2103
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation822 line 2134
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix822 line 2140
165. theorem OAI.MUB6.Certificate.PairSemantics.sound822 line 2142
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation823 line 2173
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix823 line 2179
168. theorem OAI.MUB6.Certificate.PairSemantics.sound823 line 2181
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation824 line 2212
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix824 line 2218
171. theorem OAI.MUB6.Certificate.PairSemantics.sound824 line 2220
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation825 line 2251
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix825 line 2257
174. theorem OAI.MUB6.Certificate.PairSemantics.sound825 line 2259
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation826 line 2290
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix826 line 2296
177. theorem OAI.MUB6.Certificate.PairSemantics.sound826 line 2298
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation827 line 2328
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix827 line 2334
180. theorem OAI.MUB6.Certificate.PairSemantics.sound827 line 2336
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation828 line 2366
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix828 line 2372
183. theorem OAI.MUB6.Certificate.PairSemantics.sound828 line 2374
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation829 line 2405
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix829 line 2411
186. theorem OAI.MUB6.Certificate.PairSemantics.sound829 line 2413
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation830 line 2444
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix830 line 2450
189. theorem OAI.MUB6.Certificate.PairSemantics.sound830 line 2452
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation831 line 2483
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix831 line 2489
192. theorem OAI.MUB6.Certificate.PairSemantics.sound831 line 2491