OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound13.lean

GitHub source file

190 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation832 line 71
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix832 line 77
3. theorem OAI.MUB6.Certificate.PairSemantics.sound832 line 79
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation833 line 109
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix833 line 115
6. theorem OAI.MUB6.Certificate.PairSemantics.sound833 line 117
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation834 line 147
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix834 line 153
9. theorem OAI.MUB6.Certificate.PairSemantics.sound834 line 155
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation835 line 185
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix835 line 191
12. theorem OAI.MUB6.Certificate.PairSemantics.sound835 line 193
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation836 line 223
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix836 line 229
15. theorem OAI.MUB6.Certificate.PairSemantics.sound836 line 231
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation837 line 261
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix837 line 267
18. theorem OAI.MUB6.Certificate.PairSemantics.sound837 line 269
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation838 line 299
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix838 line 305
21. theorem OAI.MUB6.Certificate.PairSemantics.sound838 line 307
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation839 line 337
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix839 line 343
24. theorem OAI.MUB6.Certificate.PairSemantics.sound839 line 345
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation840 line 375
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix840 line 381
27. theorem OAI.MUB6.Certificate.PairSemantics.sound840 line 383
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation841 line 413
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix841 line 419
30. theorem OAI.MUB6.Certificate.PairSemantics.sound841 line 421
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation842 line 452
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix842 line 458
33. theorem OAI.MUB6.Certificate.PairSemantics.sound842 line 460
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation843 line 491
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix843 line 497
36. theorem OAI.MUB6.Certificate.PairSemantics.sound843 line 499
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation844 line 529
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix844 line 535
39. theorem OAI.MUB6.Certificate.PairSemantics.sound844 line 537
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation845 line 568
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix845 line 574
42. theorem OAI.MUB6.Certificate.PairSemantics.sound845 line 576
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation846 line 606
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix846 line 612
45. theorem OAI.MUB6.Certificate.PairSemantics.sound846 line 614
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation847 line 644
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix847 line 650
48. theorem OAI.MUB6.Certificate.PairSemantics.sound847 line 652
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation848 line 682
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix848 line 688
51. theorem OAI.MUB6.Certificate.PairSemantics.sound848 line 690
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation849 line 721
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix849 line 727
54. theorem OAI.MUB6.Certificate.PairSemantics.sound849 line 729
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation850 line 760
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix850 line 766
57. theorem OAI.MUB6.Certificate.PairSemantics.sound850 line 768
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation851 line 798
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix851 line 804
60. theorem OAI.MUB6.Certificate.PairSemantics.sound851 line 806
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation852 line 837
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix852 line 843
63. theorem OAI.MUB6.Certificate.PairSemantics.sound852 line 845
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation853 line 876
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix853 line 882
66. theorem OAI.MUB6.Certificate.PairSemantics.sound853 line 884
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation854 line 914
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix854 line 920
69. theorem OAI.MUB6.Certificate.PairSemantics.sound854 line 922
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation855 line 952
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix855 line 958
72. theorem OAI.MUB6.Certificate.PairSemantics.sound855 line 960
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation856 line 995
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix856 line 1001
75. theorem OAI.MUB6.Certificate.PairSemantics.sound856 line 1003
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation857 line 1038
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix857 line 1044
78. theorem OAI.MUB6.Certificate.PairSemantics.sound857 line 1046
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation858 line 1081
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix858 line 1087
81. theorem OAI.MUB6.Certificate.PairSemantics.sound858 line 1089
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation859 line 1124
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix859 line 1130
84. theorem OAI.MUB6.Certificate.PairSemantics.sound859 line 1132
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation860 line 1167
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix860 line 1173
87. theorem OAI.MUB6.Certificate.PairSemantics.sound860 line 1175
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation861 line 1210
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix861 line 1216
90. theorem OAI.MUB6.Certificate.PairSemantics.sound861 line 1218
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation862 line 1253
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix862 line 1259
93. theorem OAI.MUB6.Certificate.PairSemantics.sound862 line 1261
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation863 line 1296
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix863 line 1302
96. theorem OAI.MUB6.Certificate.PairSemantics.sound863 line 1304
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation864 line 1339
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix864 line 1345
99. theorem OAI.MUB6.Certificate.PairSemantics.sound864 line 1347
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation865 line 1382
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix865 line 1388
102. theorem OAI.MUB6.Certificate.PairSemantics.sound865 line 1390
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation866 line 1425
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix866 line 1431
105. theorem OAI.MUB6.Certificate.PairSemantics.sound866 line 1433
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation867 line 1468
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix867 line 1474
108. theorem OAI.MUB6.Certificate.PairSemantics.sound867 line 1476
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation868 line 1511
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix868 line 1517
111. theorem OAI.MUB6.Certificate.PairSemantics.sound868 line 1519
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation869 line 1554
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix869 line 1560
114. theorem OAI.MUB6.Certificate.PairSemantics.sound869 line 1562
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation870 line 1597
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix870 line 1603
117. theorem OAI.MUB6.Certificate.PairSemantics.sound870 line 1605
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation871 line 1640
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix871 line 1646
120. theorem OAI.MUB6.Certificate.PairSemantics.sound871 line 1648
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation872 line 1683
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix872 line 1689
123. theorem OAI.MUB6.Certificate.PairSemantics.sound872 line 1691
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation873 line 1726
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix873 line 1732
126. theorem OAI.MUB6.Certificate.PairSemantics.sound873 line 1734
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation874 line 1769
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix874 line 1775
129. theorem OAI.MUB6.Certificate.PairSemantics.sound874 line 1777
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation875 line 1812
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix875 line 1818
132. theorem OAI.MUB6.Certificate.PairSemantics.sound875 line 1820
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation876 line 1855
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix876 line 1861
135. theorem OAI.MUB6.Certificate.PairSemantics.sound876 line 1863
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation877 line 1898
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix877 line 1904
138. theorem OAI.MUB6.Certificate.PairSemantics.sound877 line 1906
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation878 line 1941
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix878 line 1947
141. theorem OAI.MUB6.Certificate.PairSemantics.sound878 line 1949
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation879 line 1984
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix879 line 1990
144. theorem OAI.MUB6.Certificate.PairSemantics.sound879 line 1992
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation880 line 2027
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix880 line 2033
147. theorem OAI.MUB6.Certificate.PairSemantics.sound880 line 2035
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation881 line 2070
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix881 line 2076
150. theorem OAI.MUB6.Certificate.PairSemantics.sound881 line 2078
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation882 line 2113
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix882 line 2119
153. theorem OAI.MUB6.Certificate.PairSemantics.sound882 line 2121
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation883 line 2156
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix883 line 2162
156. theorem OAI.MUB6.Certificate.PairSemantics.sound883 line 2164
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation884 line 2199
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix884 line 2205
159. theorem OAI.MUB6.Certificate.PairSemantics.sound884 line 2207
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation885 line 2242
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix885 line 2248
162. theorem OAI.MUB6.Certificate.PairSemantics.sound885 line 2250
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation886 line 2285
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix886 line 2291
165. theorem OAI.MUB6.Certificate.PairSemantics.sound886 line 2293
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation887 line 2324
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix887 line 2330
168. theorem OAI.MUB6.Certificate.PairSemantics.sound887 line 2332
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation888 line 2363
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix888 line 2369
171. theorem OAI.MUB6.Certificate.PairSemantics.sound888 line 2371
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation889 line 2401
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix889 line 2407
174. theorem OAI.MUB6.Certificate.PairSemantics.sound889 line 2409
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation890 line 2439
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix890 line 2445
177. theorem OAI.MUB6.Certificate.PairSemantics.sound890 line 2447
178. theorem OAI.MUB6.Certificate.PairSemantics.sound891 line 2477
179. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation892 line 2482
180. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix892 line 2488
181. theorem OAI.MUB6.Certificate.PairSemantics.sound892 line 2490
182. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation893 line 2520
183. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix893 line 2526
184. theorem OAI.MUB6.Certificate.PairSemantics.sound893 line 2528
185. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation894 line 2558
186. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix894 line 2564
187. theorem OAI.MUB6.Certificate.PairSemantics.sound894 line 2566
188. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation895 line 2597
189. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix895 line 2603
190. theorem OAI.MUB6.Certificate.PairSemantics.sound895 line 2605