OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound25.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1600 line 75
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1600 line 81
3. theorem OAI.MUB6.Certificate.PairSemantics.sound1600 line 83
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1601 line 118
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1601 line 124
6. theorem OAI.MUB6.Certificate.PairSemantics.sound1601 line 126
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1602 line 161
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1602 line 167
9. theorem OAI.MUB6.Certificate.PairSemantics.sound1602 line 169
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1603 line 204
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1603 line 210
12. theorem OAI.MUB6.Certificate.PairSemantics.sound1603 line 212
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1604 line 247
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1604 line 253
15. theorem OAI.MUB6.Certificate.PairSemantics.sound1604 line 255
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1605 line 290
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1605 line 296
18. theorem OAI.MUB6.Certificate.PairSemantics.sound1605 line 298
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1606 line 333
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1606 line 339
21. theorem OAI.MUB6.Certificate.PairSemantics.sound1606 line 341
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1607 line 376
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1607 line 382
24. theorem OAI.MUB6.Certificate.PairSemantics.sound1607 line 384
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1608 line 419
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1608 line 425
27. theorem OAI.MUB6.Certificate.PairSemantics.sound1608 line 427
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1609 line 462
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1609 line 468
30. theorem OAI.MUB6.Certificate.PairSemantics.sound1609 line 470
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1610 line 505
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1610 line 511
33. theorem OAI.MUB6.Certificate.PairSemantics.sound1610 line 513
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1611 line 548
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1611 line 554
36. theorem OAI.MUB6.Certificate.PairSemantics.sound1611 line 556
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1612 line 591
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1612 line 597
39. theorem OAI.MUB6.Certificate.PairSemantics.sound1612 line 599
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1613 line 634
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1613 line 640
42. theorem OAI.MUB6.Certificate.PairSemantics.sound1613 line 642
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1614 line 677
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1614 line 683
45. theorem OAI.MUB6.Certificate.PairSemantics.sound1614 line 685
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1615 line 720
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1615 line 726
48. theorem OAI.MUB6.Certificate.PairSemantics.sound1615 line 728
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1616 line 763
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1616 line 769
51. theorem OAI.MUB6.Certificate.PairSemantics.sound1616 line 771
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1617 line 806
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1617 line 812
54. theorem OAI.MUB6.Certificate.PairSemantics.sound1617 line 814
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1618 line 849
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1618 line 855
57. theorem OAI.MUB6.Certificate.PairSemantics.sound1618 line 857
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1619 line 892
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1619 line 898
60. theorem OAI.MUB6.Certificate.PairSemantics.sound1619 line 900
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1620 line 935
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1620 line 941
63. theorem OAI.MUB6.Certificate.PairSemantics.sound1620 line 943
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1621 line 978
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1621 line 984
66. theorem OAI.MUB6.Certificate.PairSemantics.sound1621 line 986
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1622 line 1021
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1622 line 1027
69. theorem OAI.MUB6.Certificate.PairSemantics.sound1622 line 1029
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1623 line 1064
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1623 line 1070
72. theorem OAI.MUB6.Certificate.PairSemantics.sound1623 line 1072
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1624 line 1107
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1624 line 1113
75. theorem OAI.MUB6.Certificate.PairSemantics.sound1624 line 1115
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1625 line 1150
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1625 line 1156
78. theorem OAI.MUB6.Certificate.PairSemantics.sound1625 line 1158
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1626 line 1193
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1626 line 1199
81. theorem OAI.MUB6.Certificate.PairSemantics.sound1626 line 1201
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1627 line 1236
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1627 line 1242
84. theorem OAI.MUB6.Certificate.PairSemantics.sound1627 line 1244
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1628 line 1279
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1628 line 1285
87. theorem OAI.MUB6.Certificate.PairSemantics.sound1628 line 1287
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1629 line 1322
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1629 line 1328
90. theorem OAI.MUB6.Certificate.PairSemantics.sound1629 line 1330
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1630 line 1365
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1630 line 1371
93. theorem OAI.MUB6.Certificate.PairSemantics.sound1630 line 1373
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1631 line 1408
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1631 line 1414
96. theorem OAI.MUB6.Certificate.PairSemantics.sound1631 line 1416
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1632 line 1451
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1632 line 1457
99. theorem OAI.MUB6.Certificate.PairSemantics.sound1632 line 1459
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1633 line 1494
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1633 line 1500
102. theorem OAI.MUB6.Certificate.PairSemantics.sound1633 line 1502
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1634 line 1537
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1634 line 1543
105. theorem OAI.MUB6.Certificate.PairSemantics.sound1634 line 1545
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1635 line 1580
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1635 line 1586
108. theorem OAI.MUB6.Certificate.PairSemantics.sound1635 line 1588
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1636 line 1623
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1636 line 1629
111. theorem OAI.MUB6.Certificate.PairSemantics.sound1636 line 1631
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1637 line 1666
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1637 line 1672
114. theorem OAI.MUB6.Certificate.PairSemantics.sound1637 line 1674
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1638 line 1709
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1638 line 1715
117. theorem OAI.MUB6.Certificate.PairSemantics.sound1638 line 1717
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1639 line 1752
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1639 line 1758
120. theorem OAI.MUB6.Certificate.PairSemantics.sound1639 line 1760
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1640 line 1795
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1640 line 1801
123. theorem OAI.MUB6.Certificate.PairSemantics.sound1640 line 1803
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1641 line 1838
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1641 line 1844
126. theorem OAI.MUB6.Certificate.PairSemantics.sound1641 line 1846
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1642 line 1881
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1642 line 1887
129. theorem OAI.MUB6.Certificate.PairSemantics.sound1642 line 1889
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1643 line 1924
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1643 line 1930
132. theorem OAI.MUB6.Certificate.PairSemantics.sound1643 line 1932
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1644 line 1967
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1644 line 1973
135. theorem OAI.MUB6.Certificate.PairSemantics.sound1644 line 1975
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1645 line 2010
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1645 line 2016
138. theorem OAI.MUB6.Certificate.PairSemantics.sound1645 line 2018
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1646 line 2053
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1646 line 2059
141. theorem OAI.MUB6.Certificate.PairSemantics.sound1646 line 2061
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1647 line 2096
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1647 line 2102
144. theorem OAI.MUB6.Certificate.PairSemantics.sound1647 line 2104
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1648 line 2139
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1648 line 2145
147. theorem OAI.MUB6.Certificate.PairSemantics.sound1648 line 2147
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1649 line 2182
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1649 line 2188
150. theorem OAI.MUB6.Certificate.PairSemantics.sound1649 line 2190
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1650 line 2225
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1650 line 2231
153. theorem OAI.MUB6.Certificate.PairSemantics.sound1650 line 2233
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1651 line 2268
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1651 line 2274
156. theorem OAI.MUB6.Certificate.PairSemantics.sound1651 line 2276
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1652 line 2311
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1652 line 2317
159. theorem OAI.MUB6.Certificate.PairSemantics.sound1652 line 2319
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1653 line 2354
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1653 line 2360
162. theorem OAI.MUB6.Certificate.PairSemantics.sound1653 line 2362
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1654 line 2397
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1654 line 2403
165. theorem OAI.MUB6.Certificate.PairSemantics.sound1654 line 2405
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1655 line 2440
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1655 line 2446
168. theorem OAI.MUB6.Certificate.PairSemantics.sound1655 line 2448
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1656 line 2483
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1656 line 2489
171. theorem OAI.MUB6.Certificate.PairSemantics.sound1656 line 2491
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1657 line 2526
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1657 line 2532
174. theorem OAI.MUB6.Certificate.PairSemantics.sound1657 line 2534
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1658 line 2569
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1658 line 2575
177. theorem OAI.MUB6.Certificate.PairSemantics.sound1658 line 2577
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1659 line 2612
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1659 line 2618
180. theorem OAI.MUB6.Certificate.PairSemantics.sound1659 line 2620
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1660 line 2655
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1660 line 2661
183. theorem OAI.MUB6.Certificate.PairSemantics.sound1660 line 2663
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1661 line 2698
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1661 line 2704
186. theorem OAI.MUB6.Certificate.PairSemantics.sound1661 line 2706
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1662 line 2741
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1662 line 2747
189. theorem OAI.MUB6.Certificate.PairSemantics.sound1662 line 2749
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation1663 line 2784
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix1663 line 2790
192. theorem OAI.MUB6.Certificate.PairSemantics.sound1663 line 2792