OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound40.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2560 line 74
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2560 line 80
3. theorem OAI.MUB6.Certificate.PairSemantics.sound2560 line 82
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2561 line 117
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2561 line 123
6. theorem OAI.MUB6.Certificate.PairSemantics.sound2561 line 125
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2562 line 160
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2562 line 166
9. theorem OAI.MUB6.Certificate.PairSemantics.sound2562 line 168
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2563 line 203
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2563 line 209
12. theorem OAI.MUB6.Certificate.PairSemantics.sound2563 line 211
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2564 line 246
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2564 line 252
15. theorem OAI.MUB6.Certificate.PairSemantics.sound2564 line 254
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2565 line 289
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2565 line 295
18. theorem OAI.MUB6.Certificate.PairSemantics.sound2565 line 297
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2566 line 332
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2566 line 338
21. theorem OAI.MUB6.Certificate.PairSemantics.sound2566 line 340
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2567 line 375
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2567 line 381
24. theorem OAI.MUB6.Certificate.PairSemantics.sound2567 line 383
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2568 line 418
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2568 line 424
27. theorem OAI.MUB6.Certificate.PairSemantics.sound2568 line 426
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2569 line 461
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2569 line 467
30. theorem OAI.MUB6.Certificate.PairSemantics.sound2569 line 469
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2570 line 504
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2570 line 510
33. theorem OAI.MUB6.Certificate.PairSemantics.sound2570 line 512
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2571 line 547
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2571 line 553
36. theorem OAI.MUB6.Certificate.PairSemantics.sound2571 line 555
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2572 line 590
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2572 line 596
39. theorem OAI.MUB6.Certificate.PairSemantics.sound2572 line 598
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2573 line 633
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2573 line 639
42. theorem OAI.MUB6.Certificate.PairSemantics.sound2573 line 641
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2574 line 676
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2574 line 682
45. theorem OAI.MUB6.Certificate.PairSemantics.sound2574 line 684
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2575 line 719
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2575 line 725
48. theorem OAI.MUB6.Certificate.PairSemantics.sound2575 line 727
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2576 line 762
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2576 line 768
51. theorem OAI.MUB6.Certificate.PairSemantics.sound2576 line 770
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2577 line 805
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2577 line 811
54. theorem OAI.MUB6.Certificate.PairSemantics.sound2577 line 813
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2578 line 848
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2578 line 854
57. theorem OAI.MUB6.Certificate.PairSemantics.sound2578 line 856
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2579 line 891
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2579 line 897
60. theorem OAI.MUB6.Certificate.PairSemantics.sound2579 line 899
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2580 line 934
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2580 line 940
63. theorem OAI.MUB6.Certificate.PairSemantics.sound2580 line 942
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2581 line 977
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2581 line 983
66. theorem OAI.MUB6.Certificate.PairSemantics.sound2581 line 985
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2582 line 1020
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2582 line 1026
69. theorem OAI.MUB6.Certificate.PairSemantics.sound2582 line 1028
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2583 line 1063
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2583 line 1069
72. theorem OAI.MUB6.Certificate.PairSemantics.sound2583 line 1071
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2584 line 1106
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2584 line 1112
75. theorem OAI.MUB6.Certificate.PairSemantics.sound2584 line 1114
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2585 line 1149
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2585 line 1155
78. theorem OAI.MUB6.Certificate.PairSemantics.sound2585 line 1157
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2586 line 1192
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2586 line 1198
81. theorem OAI.MUB6.Certificate.PairSemantics.sound2586 line 1200
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2587 line 1235
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2587 line 1241
84. theorem OAI.MUB6.Certificate.PairSemantics.sound2587 line 1243
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2588 line 1278
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2588 line 1284
87. theorem OAI.MUB6.Certificate.PairSemantics.sound2588 line 1286
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2589 line 1321
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2589 line 1327
90. theorem OAI.MUB6.Certificate.PairSemantics.sound2589 line 1329
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2590 line 1364
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2590 line 1370
93. theorem OAI.MUB6.Certificate.PairSemantics.sound2590 line 1372
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2591 line 1407
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2591 line 1413
96. theorem OAI.MUB6.Certificate.PairSemantics.sound2591 line 1415
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2592 line 1450
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2592 line 1456
99. theorem OAI.MUB6.Certificate.PairSemantics.sound2592 line 1458
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2593 line 1493
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2593 line 1499
102. theorem OAI.MUB6.Certificate.PairSemantics.sound2593 line 1501
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2594 line 1536
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2594 line 1542
105. theorem OAI.MUB6.Certificate.PairSemantics.sound2594 line 1544
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2595 line 1579
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2595 line 1585
108. theorem OAI.MUB6.Certificate.PairSemantics.sound2595 line 1587
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2596 line 1622
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2596 line 1628
111. theorem OAI.MUB6.Certificate.PairSemantics.sound2596 line 1630
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2597 line 1665
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2597 line 1671
114. theorem OAI.MUB6.Certificate.PairSemantics.sound2597 line 1673
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2598 line 1708
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2598 line 1714
117. theorem OAI.MUB6.Certificate.PairSemantics.sound2598 line 1716
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2599 line 1751
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2599 line 1757
120. theorem OAI.MUB6.Certificate.PairSemantics.sound2599 line 1759
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2600 line 1794
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2600 line 1800
123. theorem OAI.MUB6.Certificate.PairSemantics.sound2600 line 1802
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2601 line 1837
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2601 line 1843
126. theorem OAI.MUB6.Certificate.PairSemantics.sound2601 line 1845
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2602 line 1880
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2602 line 1886
129. theorem OAI.MUB6.Certificate.PairSemantics.sound2602 line 1888
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2603 line 1923
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2603 line 1929
132. theorem OAI.MUB6.Certificate.PairSemantics.sound2603 line 1931
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2604 line 1966
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2604 line 1972
135. theorem OAI.MUB6.Certificate.PairSemantics.sound2604 line 1974
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2605 line 2009
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2605 line 2015
138. theorem OAI.MUB6.Certificate.PairSemantics.sound2605 line 2017
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2606 line 2052
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2606 line 2058
141. theorem OAI.MUB6.Certificate.PairSemantics.sound2606 line 2060
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2607 line 2095
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2607 line 2101
144. theorem OAI.MUB6.Certificate.PairSemantics.sound2607 line 2103
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2608 line 2138
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2608 line 2144
147. theorem OAI.MUB6.Certificate.PairSemantics.sound2608 line 2146
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2609 line 2181
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2609 line 2187
150. theorem OAI.MUB6.Certificate.PairSemantics.sound2609 line 2189
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2610 line 2224
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2610 line 2230
153. theorem OAI.MUB6.Certificate.PairSemantics.sound2610 line 2232
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2611 line 2267
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2611 line 2273
156. theorem OAI.MUB6.Certificate.PairSemantics.sound2611 line 2275
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2612 line 2310
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2612 line 2316
159. theorem OAI.MUB6.Certificate.PairSemantics.sound2612 line 2318
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2613 line 2353
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2613 line 2359
162. theorem OAI.MUB6.Certificate.PairSemantics.sound2613 line 2361
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2614 line 2396
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2614 line 2402
165. theorem OAI.MUB6.Certificate.PairSemantics.sound2614 line 2404
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2615 line 2439
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2615 line 2445
168. theorem OAI.MUB6.Certificate.PairSemantics.sound2615 line 2447
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2616 line 2482
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2616 line 2488
171. theorem OAI.MUB6.Certificate.PairSemantics.sound2616 line 2490
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2617 line 2525
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2617 line 2531
174. theorem OAI.MUB6.Certificate.PairSemantics.sound2617 line 2533
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2618 line 2568
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2618 line 2574
177. theorem OAI.MUB6.Certificate.PairSemantics.sound2618 line 2576
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2619 line 2611
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2619 line 2617
180. theorem OAI.MUB6.Certificate.PairSemantics.sound2619 line 2619
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2620 line 2654
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2620 line 2660
183. theorem OAI.MUB6.Certificate.PairSemantics.sound2620 line 2662
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2621 line 2697
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2621 line 2703
186. theorem OAI.MUB6.Certificate.PairSemantics.sound2621 line 2705
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2622 line 2740
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2622 line 2746
189. theorem OAI.MUB6.Certificate.PairSemantics.sound2622 line 2748
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2623 line 2783
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2623 line 2789
192. theorem OAI.MUB6.Certificate.PairSemantics.sound2623 line 2791