OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound26.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1664 line 77
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1664 line 83
3. theorem OAI.MUB6.Certificate.PairSemantics.sound1664 line 85
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1665 line 120
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1665 line 126
6. theorem OAI.MUB6.Certificate.PairSemantics.sound1665 line 128
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1666 line 163
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1666 line 169
9. theorem OAI.MUB6.Certificate.PairSemantics.sound1666 line 171
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1667 line 206
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1667 line 212
12. theorem OAI.MUB6.Certificate.PairSemantics.sound1667 line 214
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1668 line 249
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1668 line 255
15. theorem OAI.MUB6.Certificate.PairSemantics.sound1668 line 257
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1669 line 292
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1669 line 298
18. theorem OAI.MUB6.Certificate.PairSemantics.sound1669 line 300
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1670 line 335
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1670 line 341
21. theorem OAI.MUB6.Certificate.PairSemantics.sound1670 line 343
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1671 line 378
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1671 line 384
24. theorem OAI.MUB6.Certificate.PairSemantics.sound1671 line 386
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1672 line 421
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1672 line 427
27. theorem OAI.MUB6.Certificate.PairSemantics.sound1672 line 429
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1673 line 464
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1673 line 470
30. theorem OAI.MUB6.Certificate.PairSemantics.sound1673 line 472
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1674 line 507
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1674 line 513
33. theorem OAI.MUB6.Certificate.PairSemantics.sound1674 line 515
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1675 line 550
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1675 line 556
36. theorem OAI.MUB6.Certificate.PairSemantics.sound1675 line 558
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1676 line 593
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1676 line 599
39. theorem OAI.MUB6.Certificate.PairSemantics.sound1676 line 601
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1677 line 636
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1677 line 642
42. theorem OAI.MUB6.Certificate.PairSemantics.sound1677 line 644
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1678 line 679
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1678 line 685
45. theorem OAI.MUB6.Certificate.PairSemantics.sound1678 line 687
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1679 line 722
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1679 line 728
48. theorem OAI.MUB6.Certificate.PairSemantics.sound1679 line 730
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1680 line 765
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1680 line 771
51. theorem OAI.MUB6.Certificate.PairSemantics.sound1680 line 773
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1681 line 808
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1681 line 814
54. theorem OAI.MUB6.Certificate.PairSemantics.sound1681 line 816
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1682 line 851
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1682 line 857
57. theorem OAI.MUB6.Certificate.PairSemantics.sound1682 line 859
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1683 line 894
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1683 line 900
60. theorem OAI.MUB6.Certificate.PairSemantics.sound1683 line 902
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1684 line 937
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1684 line 943
63. theorem OAI.MUB6.Certificate.PairSemantics.sound1684 line 945
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1685 line 980
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1685 line 986
66. theorem OAI.MUB6.Certificate.PairSemantics.sound1685 line 988
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1686 line 1023
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1686 line 1029
69. theorem OAI.MUB6.Certificate.PairSemantics.sound1686 line 1031
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1687 line 1066
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1687 line 1072
72. theorem OAI.MUB6.Certificate.PairSemantics.sound1687 line 1074
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1688 line 1109
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1688 line 1115
75. theorem OAI.MUB6.Certificate.PairSemantics.sound1688 line 1117
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1689 line 1152
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1689 line 1158
78. theorem OAI.MUB6.Certificate.PairSemantics.sound1689 line 1160
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1690 line 1195
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1690 line 1201
81. theorem OAI.MUB6.Certificate.PairSemantics.sound1690 line 1203
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1691 line 1238
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1691 line 1244
84. theorem OAI.MUB6.Certificate.PairSemantics.sound1691 line 1246
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1692 line 1281
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1692 line 1287
87. theorem OAI.MUB6.Certificate.PairSemantics.sound1692 line 1289
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1693 line 1324
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1693 line 1330
90. theorem OAI.MUB6.Certificate.PairSemantics.sound1693 line 1332
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1694 line 1367
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1694 line 1373
93. theorem OAI.MUB6.Certificate.PairSemantics.sound1694 line 1375
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1695 line 1410
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1695 line 1416
96. theorem OAI.MUB6.Certificate.PairSemantics.sound1695 line 1418
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1696 line 1453
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1696 line 1459
99. theorem OAI.MUB6.Certificate.PairSemantics.sound1696 line 1461
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1697 line 1496
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1697 line 1502
102. theorem OAI.MUB6.Certificate.PairSemantics.sound1697 line 1504
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1698 line 1539
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1698 line 1545
105. theorem OAI.MUB6.Certificate.PairSemantics.sound1698 line 1547
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1699 line 1582
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1699 line 1588
108. theorem OAI.MUB6.Certificate.PairSemantics.sound1699 line 1590
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1700 line 1625
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1700 line 1631
111. theorem OAI.MUB6.Certificate.PairSemantics.sound1700 line 1633
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1701 line 1668
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1701 line 1674
114. theorem OAI.MUB6.Certificate.PairSemantics.sound1701 line 1676
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1702 line 1711
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1702 line 1717
117. theorem OAI.MUB6.Certificate.PairSemantics.sound1702 line 1719
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1703 line 1754
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1703 line 1760
120. theorem OAI.MUB6.Certificate.PairSemantics.sound1703 line 1762
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1704 line 1797
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1704 line 1803
123. theorem OAI.MUB6.Certificate.PairSemantics.sound1704 line 1805
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1705 line 1840
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1705 line 1846
126. theorem OAI.MUB6.Certificate.PairSemantics.sound1705 line 1848
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1706 line 1883
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1706 line 1889
129. theorem OAI.MUB6.Certificate.PairSemantics.sound1706 line 1891
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1707 line 1926
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1707 line 1932
132. theorem OAI.MUB6.Certificate.PairSemantics.sound1707 line 1934
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1708 line 1969
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1708 line 1975
135. theorem OAI.MUB6.Certificate.PairSemantics.sound1708 line 1977
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1709 line 2012
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1709 line 2018
138. theorem OAI.MUB6.Certificate.PairSemantics.sound1709 line 2020
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1710 line 2055
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1710 line 2061
141. theorem OAI.MUB6.Certificate.PairSemantics.sound1710 line 2063
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1711 line 2098
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1711 line 2104
144. theorem OAI.MUB6.Certificate.PairSemantics.sound1711 line 2106
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1712 line 2141
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1712 line 2147
147. theorem OAI.MUB6.Certificate.PairSemantics.sound1712 line 2149
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1713 line 2184
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1713 line 2190
150. theorem OAI.MUB6.Certificate.PairSemantics.sound1713 line 2192
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1714 line 2227
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1714 line 2233
153. theorem OAI.MUB6.Certificate.PairSemantics.sound1714 line 2235
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1715 line 2270
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1715 line 2276
156. theorem OAI.MUB6.Certificate.PairSemantics.sound1715 line 2278
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1716 line 2313
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1716 line 2319
159. theorem OAI.MUB6.Certificate.PairSemantics.sound1716 line 2321
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1717 line 2356
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1717 line 2362
162. theorem OAI.MUB6.Certificate.PairSemantics.sound1717 line 2364
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1718 line 2399
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1718 line 2405
165. theorem OAI.MUB6.Certificate.PairSemantics.sound1718 line 2407
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1719 line 2442
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1719 line 2448
168. theorem OAI.MUB6.Certificate.PairSemantics.sound1719 line 2450
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1720 line 2485
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1720 line 2491
171. theorem OAI.MUB6.Certificate.PairSemantics.sound1720 line 2493
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1721 line 2528
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1721 line 2534
174. theorem OAI.MUB6.Certificate.PairSemantics.sound1721 line 2536
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1722 line 2571
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1722 line 2577
177. theorem OAI.MUB6.Certificate.PairSemantics.sound1722 line 2579
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1723 line 2614
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1723 line 2620
180. theorem OAI.MUB6.Certificate.PairSemantics.sound1723 line 2622
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1724 line 2657
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1724 line 2663
183. theorem OAI.MUB6.Certificate.PairSemantics.sound1724 line 2665
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1725 line 2700
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1725 line 2706
186. theorem OAI.MUB6.Certificate.PairSemantics.sound1725 line 2708
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1726 line 2743
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1726 line 2749
189. theorem OAI.MUB6.Certificate.PairSemantics.sound1726 line 2751
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1727 line 2786
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1727 line 2792
192. theorem OAI.MUB6.Certificate.PairSemantics.sound1727 line 2794