OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound41.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2624 line 89
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2624 line 95
3. theorem OAI.MUB6.Certificate.PairSemantics.sound2624 line 97
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2625 line 132
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2625 line 138
6. theorem OAI.MUB6.Certificate.PairSemantics.sound2625 line 140
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2626 line 175
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2626 line 181
9. theorem OAI.MUB6.Certificate.PairSemantics.sound2626 line 183
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2627 line 218
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2627 line 224
12. theorem OAI.MUB6.Certificate.PairSemantics.sound2627 line 226
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2628 line 261
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2628 line 267
15. theorem OAI.MUB6.Certificate.PairSemantics.sound2628 line 269
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2629 line 304
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2629 line 310
18. theorem OAI.MUB6.Certificate.PairSemantics.sound2629 line 312
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2630 line 347
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2630 line 353
21. theorem OAI.MUB6.Certificate.PairSemantics.sound2630 line 355
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2631 line 390
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2631 line 396
24. theorem OAI.MUB6.Certificate.PairSemantics.sound2631 line 398
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2632 line 433
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2632 line 439
27. theorem OAI.MUB6.Certificate.PairSemantics.sound2632 line 441
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2633 line 476
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2633 line 482
30. theorem OAI.MUB6.Certificate.PairSemantics.sound2633 line 484
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2634 line 519
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2634 line 525
33. theorem OAI.MUB6.Certificate.PairSemantics.sound2634 line 527
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2635 line 562
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2635 line 568
36. theorem OAI.MUB6.Certificate.PairSemantics.sound2635 line 570
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2636 line 605
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2636 line 611
39. theorem OAI.MUB6.Certificate.PairSemantics.sound2636 line 613
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2637 line 648
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2637 line 654
42. theorem OAI.MUB6.Certificate.PairSemantics.sound2637 line 656
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2638 line 691
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2638 line 697
45. theorem OAI.MUB6.Certificate.PairSemantics.sound2638 line 699
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2639 line 734
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2639 line 740
48. theorem OAI.MUB6.Certificate.PairSemantics.sound2639 line 742
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2640 line 777
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2640 line 783
51. theorem OAI.MUB6.Certificate.PairSemantics.sound2640 line 785
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2641 line 820
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2641 line 826
54. theorem OAI.MUB6.Certificate.PairSemantics.sound2641 line 828
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2642 line 863
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2642 line 869
57. theorem OAI.MUB6.Certificate.PairSemantics.sound2642 line 871
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2643 line 906
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2643 line 912
60. theorem OAI.MUB6.Certificate.PairSemantics.sound2643 line 914
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2644 line 949
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2644 line 955
63. theorem OAI.MUB6.Certificate.PairSemantics.sound2644 line 957
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2645 line 992
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2645 line 998
66. theorem OAI.MUB6.Certificate.PairSemantics.sound2645 line 1000
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2646 line 1035
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2646 line 1041
69. theorem OAI.MUB6.Certificate.PairSemantics.sound2646 line 1043
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2647 line 1078
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2647 line 1084
72. theorem OAI.MUB6.Certificate.PairSemantics.sound2647 line 1086
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2648 line 1121
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2648 line 1127
75. theorem OAI.MUB6.Certificate.PairSemantics.sound2648 line 1129
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2649 line 1169
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2649 line 1175
78. theorem OAI.MUB6.Certificate.PairSemantics.sound2649 line 1177
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2650 line 1217
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2650 line 1223
81. theorem OAI.MUB6.Certificate.PairSemantics.sound2650 line 1225
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2651 line 1265
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2651 line 1271
84. theorem OAI.MUB6.Certificate.PairSemantics.sound2651 line 1273
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2652 line 1313
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2652 line 1319
87. theorem OAI.MUB6.Certificate.PairSemantics.sound2652 line 1321
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2653 line 1361
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2653 line 1367
90. theorem OAI.MUB6.Certificate.PairSemantics.sound2653 line 1369
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2654 line 1409
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2654 line 1415
93. theorem OAI.MUB6.Certificate.PairSemantics.sound2654 line 1417
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2655 line 1457
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2655 line 1463
96. theorem OAI.MUB6.Certificate.PairSemantics.sound2655 line 1465
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2656 line 1505
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2656 line 1511
99. theorem OAI.MUB6.Certificate.PairSemantics.sound2656 line 1513
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2657 line 1553
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2657 line 1559
102. theorem OAI.MUB6.Certificate.PairSemantics.sound2657 line 1561
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2658 line 1601
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2658 line 1607
105. theorem OAI.MUB6.Certificate.PairSemantics.sound2658 line 1609
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2659 line 1649
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2659 line 1655
108. theorem OAI.MUB6.Certificate.PairSemantics.sound2659 line 1657
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2660 line 1697
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2660 line 1703
111. theorem OAI.MUB6.Certificate.PairSemantics.sound2660 line 1705
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2661 line 1745
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2661 line 1751
114. theorem OAI.MUB6.Certificate.PairSemantics.sound2661 line 1753
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2662 line 1793
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2662 line 1799
117. theorem OAI.MUB6.Certificate.PairSemantics.sound2662 line 1801
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2663 line 1841
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2663 line 1847
120. theorem OAI.MUB6.Certificate.PairSemantics.sound2663 line 1849
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2664 line 1889
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2664 line 1895
123. theorem OAI.MUB6.Certificate.PairSemantics.sound2664 line 1897
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2665 line 1937
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2665 line 1943
126. theorem OAI.MUB6.Certificate.PairSemantics.sound2665 line 1945
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2666 line 1985
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2666 line 1991
129. theorem OAI.MUB6.Certificate.PairSemantics.sound2666 line 1993
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2667 line 2033
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2667 line 2039
132. theorem OAI.MUB6.Certificate.PairSemantics.sound2667 line 2041
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2668 line 2081
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2668 line 2087
135. theorem OAI.MUB6.Certificate.PairSemantics.sound2668 line 2089
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2669 line 2129
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2669 line 2135
138. theorem OAI.MUB6.Certificate.PairSemantics.sound2669 line 2137
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2670 line 2177
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2670 line 2183
141. theorem OAI.MUB6.Certificate.PairSemantics.sound2670 line 2185
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2671 line 2225
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2671 line 2231
144. theorem OAI.MUB6.Certificate.PairSemantics.sound2671 line 2233
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2672 line 2273
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2672 line 2279
147. theorem OAI.MUB6.Certificate.PairSemantics.sound2672 line 2281
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2673 line 2321
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2673 line 2327
150. theorem OAI.MUB6.Certificate.PairSemantics.sound2673 line 2329
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2674 line 2369
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2674 line 2375
153. theorem OAI.MUB6.Certificate.PairSemantics.sound2674 line 2377
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2675 line 2417
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2675 line 2423
156. theorem OAI.MUB6.Certificate.PairSemantics.sound2675 line 2425
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2676 line 2465
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2676 line 2471
159. theorem OAI.MUB6.Certificate.PairSemantics.sound2676 line 2473
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2677 line 2508
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2677 line 2514
162. theorem OAI.MUB6.Certificate.PairSemantics.sound2677 line 2516
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2678 line 2551
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2678 line 2557
165. theorem OAI.MUB6.Certificate.PairSemantics.sound2678 line 2559
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2679 line 2594
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2679 line 2600
168. theorem OAI.MUB6.Certificate.PairSemantics.sound2679 line 2602
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2680 line 2637
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2680 line 2643
171. theorem OAI.MUB6.Certificate.PairSemantics.sound2680 line 2645
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2681 line 2680
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2681 line 2686
174. theorem OAI.MUB6.Certificate.PairSemantics.sound2681 line 2688
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2682 line 2723
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2682 line 2729
177. theorem OAI.MUB6.Certificate.PairSemantics.sound2682 line 2731
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2683 line 2766
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2683 line 2772
180. theorem OAI.MUB6.Certificate.PairSemantics.sound2683 line 2774
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2684 line 2809
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2684 line 2815
183. theorem OAI.MUB6.Certificate.PairSemantics.sound2684 line 2817
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2685 line 2852
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2685 line 2858
186. theorem OAI.MUB6.Certificate.PairSemantics.sound2685 line 2860
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2686 line 2895
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2686 line 2901
189. theorem OAI.MUB6.Certificate.PairSemantics.sound2686 line 2903
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2687 line 2938
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2687 line 2944
192. theorem OAI.MUB6.Certificate.PairSemantics.sound2687 line 2946