OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound27.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1728 line 71
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1728 line 77
3. theorem OAI.MUB6.Certificate.PairSemantics.sound1728 line 79
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1729 line 114
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1729 line 120
6. theorem OAI.MUB6.Certificate.PairSemantics.sound1729 line 122
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1730 line 157
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1730 line 163
9. theorem OAI.MUB6.Certificate.PairSemantics.sound1730 line 165
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1731 line 200
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1731 line 206
12. theorem OAI.MUB6.Certificate.PairSemantics.sound1731 line 208
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1732 line 243
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1732 line 249
15. theorem OAI.MUB6.Certificate.PairSemantics.sound1732 line 251
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1733 line 286
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1733 line 292
18. theorem OAI.MUB6.Certificate.PairSemantics.sound1733 line 294
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1734 line 329
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1734 line 335
21. theorem OAI.MUB6.Certificate.PairSemantics.sound1734 line 337
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1735 line 372
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1735 line 378
24. theorem OAI.MUB6.Certificate.PairSemantics.sound1735 line 380
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1736 line 415
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1736 line 421
27. theorem OAI.MUB6.Certificate.PairSemantics.sound1736 line 423
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1737 line 458
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1737 line 464
30. theorem OAI.MUB6.Certificate.PairSemantics.sound1737 line 466
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1738 line 501
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1738 line 507
33. theorem OAI.MUB6.Certificate.PairSemantics.sound1738 line 509
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1739 line 544
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1739 line 550
36. theorem OAI.MUB6.Certificate.PairSemantics.sound1739 line 552
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1740 line 587
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1740 line 593
39. theorem OAI.MUB6.Certificate.PairSemantics.sound1740 line 595
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1741 line 630
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1741 line 636
42. theorem OAI.MUB6.Certificate.PairSemantics.sound1741 line 638
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1742 line 673
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1742 line 679
45. theorem OAI.MUB6.Certificate.PairSemantics.sound1742 line 681
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1743 line 716
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1743 line 722
48. theorem OAI.MUB6.Certificate.PairSemantics.sound1743 line 724
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1744 line 759
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1744 line 765
51. theorem OAI.MUB6.Certificate.PairSemantics.sound1744 line 767
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1745 line 802
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1745 line 808
54. theorem OAI.MUB6.Certificate.PairSemantics.sound1745 line 810
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1746 line 845
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1746 line 851
57. theorem OAI.MUB6.Certificate.PairSemantics.sound1746 line 853
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1747 line 888
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1747 line 894
60. theorem OAI.MUB6.Certificate.PairSemantics.sound1747 line 896
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1748 line 931
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1748 line 937
63. theorem OAI.MUB6.Certificate.PairSemantics.sound1748 line 939
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1749 line 974
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1749 line 980
66. theorem OAI.MUB6.Certificate.PairSemantics.sound1749 line 982
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1750 line 1017
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1750 line 1023
69. theorem OAI.MUB6.Certificate.PairSemantics.sound1750 line 1025
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1751 line 1060
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1751 line 1066
72. theorem OAI.MUB6.Certificate.PairSemantics.sound1751 line 1068
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1752 line 1103
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1752 line 1109
75. theorem OAI.MUB6.Certificate.PairSemantics.sound1752 line 1111
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1753 line 1146
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1753 line 1152
78. theorem OAI.MUB6.Certificate.PairSemantics.sound1753 line 1154
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1754 line 1189
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1754 line 1195
81. theorem OAI.MUB6.Certificate.PairSemantics.sound1754 line 1197
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1755 line 1232
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1755 line 1238
84. theorem OAI.MUB6.Certificate.PairSemantics.sound1755 line 1240
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1756 line 1275
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1756 line 1281
87. theorem OAI.MUB6.Certificate.PairSemantics.sound1756 line 1283
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1757 line 1318
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1757 line 1324
90. theorem OAI.MUB6.Certificate.PairSemantics.sound1757 line 1326
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1758 line 1361
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1758 line 1367
93. theorem OAI.MUB6.Certificate.PairSemantics.sound1758 line 1369
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1759 line 1404
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1759 line 1410
96. theorem OAI.MUB6.Certificate.PairSemantics.sound1759 line 1412
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1760 line 1447
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1760 line 1453
99. theorem OAI.MUB6.Certificate.PairSemantics.sound1760 line 1455
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1761 line 1490
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1761 line 1496
102. theorem OAI.MUB6.Certificate.PairSemantics.sound1761 line 1498
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1762 line 1533
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1762 line 1539
105. theorem OAI.MUB6.Certificate.PairSemantics.sound1762 line 1541
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1763 line 1576
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1763 line 1582
108. theorem OAI.MUB6.Certificate.PairSemantics.sound1763 line 1584
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1764 line 1619
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1764 line 1625
111. theorem OAI.MUB6.Certificate.PairSemantics.sound1764 line 1627
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1765 line 1662
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1765 line 1668
114. theorem OAI.MUB6.Certificate.PairSemantics.sound1765 line 1670
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1766 line 1705
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1766 line 1711
117. theorem OAI.MUB6.Certificate.PairSemantics.sound1766 line 1713
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1767 line 1748
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1767 line 1754
120. theorem OAI.MUB6.Certificate.PairSemantics.sound1767 line 1756
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1768 line 1791
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1768 line 1797
123. theorem OAI.MUB6.Certificate.PairSemantics.sound1768 line 1799
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1769 line 1834
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1769 line 1840
126. theorem OAI.MUB6.Certificate.PairSemantics.sound1769 line 1842
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1770 line 1877
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1770 line 1883
129. theorem OAI.MUB6.Certificate.PairSemantics.sound1770 line 1885
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1771 line 1920
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1771 line 1926
132. theorem OAI.MUB6.Certificate.PairSemantics.sound1771 line 1928
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1772 line 1963
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1772 line 1969
135. theorem OAI.MUB6.Certificate.PairSemantics.sound1772 line 1971
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1773 line 2006
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1773 line 2012
138. theorem OAI.MUB6.Certificate.PairSemantics.sound1773 line 2014
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1774 line 2049
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1774 line 2055
141. theorem OAI.MUB6.Certificate.PairSemantics.sound1774 line 2057
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1775 line 2092
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1775 line 2098
144. theorem OAI.MUB6.Certificate.PairSemantics.sound1775 line 2100
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1776 line 2135
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1776 line 2141
147. theorem OAI.MUB6.Certificate.PairSemantics.sound1776 line 2143
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1777 line 2178
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1777 line 2184
150. theorem OAI.MUB6.Certificate.PairSemantics.sound1777 line 2186
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1778 line 2221
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1778 line 2227
153. theorem OAI.MUB6.Certificate.PairSemantics.sound1778 line 2229
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1779 line 2264
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1779 line 2270
156. theorem OAI.MUB6.Certificate.PairSemantics.sound1779 line 2272
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1780 line 2307
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1780 line 2313
159. theorem OAI.MUB6.Certificate.PairSemantics.sound1780 line 2315
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1781 line 2350
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1781 line 2356
162. theorem OAI.MUB6.Certificate.PairSemantics.sound1781 line 2358
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1782 line 2393
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1782 line 2399
165. theorem OAI.MUB6.Certificate.PairSemantics.sound1782 line 2401
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1783 line 2436
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1783 line 2442
168. theorem OAI.MUB6.Certificate.PairSemantics.sound1783 line 2444
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1784 line 2479
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1784 line 2485
171. theorem OAI.MUB6.Certificate.PairSemantics.sound1784 line 2487
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1785 line 2522
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1785 line 2528
174. theorem OAI.MUB6.Certificate.PairSemantics.sound1785 line 2530
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1786 line 2565
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1786 line 2571
177. theorem OAI.MUB6.Certificate.PairSemantics.sound1786 line 2573
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1787 line 2608
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1787 line 2614
180. theorem OAI.MUB6.Certificate.PairSemantics.sound1787 line 2616
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1788 line 2651
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1788 line 2657
183. theorem OAI.MUB6.Certificate.PairSemantics.sound1788 line 2659
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1789 line 2694
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1789 line 2700
186. theorem OAI.MUB6.Certificate.PairSemantics.sound1789 line 2702
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1790 line 2737
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1790 line 2743
189. theorem OAI.MUB6.Certificate.PairSemantics.sound1790 line 2745
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1791 line 2780
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1791 line 2786
192. theorem OAI.MUB6.Certificate.PairSemantics.sound1791 line 2788