OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound43.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2752 line 122
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2752 line 128
3. theorem OAI.MUB6.Certificate.PairSemantics.sound2752 line 130
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2753 line 165
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2753 line 171
6. theorem OAI.MUB6.Certificate.PairSemantics.sound2753 line 173
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2754 line 208
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2754 line 214
9. theorem OAI.MUB6.Certificate.PairSemantics.sound2754 line 216
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2755 line 251
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2755 line 257
12. theorem OAI.MUB6.Certificate.PairSemantics.sound2755 line 259
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2756 line 294
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2756 line 300
15. theorem OAI.MUB6.Certificate.PairSemantics.sound2756 line 302
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2757 line 337
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2757 line 343
18. theorem OAI.MUB6.Certificate.PairSemantics.sound2757 line 345
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2758 line 380
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2758 line 386
21. theorem OAI.MUB6.Certificate.PairSemantics.sound2758 line 388
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2759 line 423
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2759 line 429
24. theorem OAI.MUB6.Certificate.PairSemantics.sound2759 line 431
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2760 line 466
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2760 line 472
27. theorem OAI.MUB6.Certificate.PairSemantics.sound2760 line 474
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2761 line 509
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2761 line 515
30. theorem OAI.MUB6.Certificate.PairSemantics.sound2761 line 517
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2762 line 552
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2762 line 558
33. theorem OAI.MUB6.Certificate.PairSemantics.sound2762 line 560
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2763 line 595
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2763 line 601
36. theorem OAI.MUB6.Certificate.PairSemantics.sound2763 line 603
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2764 line 638
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2764 line 644
39. theorem OAI.MUB6.Certificate.PairSemantics.sound2764 line 646
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2765 line 681
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2765 line 687
42. theorem OAI.MUB6.Certificate.PairSemantics.sound2765 line 689
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2766 line 724
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2766 line 730
45. theorem OAI.MUB6.Certificate.PairSemantics.sound2766 line 732
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2767 line 767
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2767 line 773
48. theorem OAI.MUB6.Certificate.PairSemantics.sound2767 line 775
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2768 line 810
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2768 line 816
51. theorem OAI.MUB6.Certificate.PairSemantics.sound2768 line 818
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2769 line 853
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2769 line 859
54. theorem OAI.MUB6.Certificate.PairSemantics.sound2769 line 861
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2770 line 896
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2770 line 902
57. theorem OAI.MUB6.Certificate.PairSemantics.sound2770 line 904
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2771 line 939
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2771 line 945
60. theorem OAI.MUB6.Certificate.PairSemantics.sound2771 line 947
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2772 line 982
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2772 line 988
63. theorem OAI.MUB6.Certificate.PairSemantics.sound2772 line 990
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2773 line 1025
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2773 line 1031
66. theorem OAI.MUB6.Certificate.PairSemantics.sound2773 line 1033
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2774 line 1068
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2774 line 1074
69. theorem OAI.MUB6.Certificate.PairSemantics.sound2774 line 1076
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2775 line 1111
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2775 line 1117
72. theorem OAI.MUB6.Certificate.PairSemantics.sound2775 line 1119
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2776 line 1154
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2776 line 1160
75. theorem OAI.MUB6.Certificate.PairSemantics.sound2776 line 1162
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2777 line 1197
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2777 line 1203
78. theorem OAI.MUB6.Certificate.PairSemantics.sound2777 line 1205
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2778 line 1240
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2778 line 1246
81. theorem OAI.MUB6.Certificate.PairSemantics.sound2778 line 1248
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2779 line 1283
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2779 line 1289
84. theorem OAI.MUB6.Certificate.PairSemantics.sound2779 line 1291
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2780 line 1326
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2780 line 1332
87. theorem OAI.MUB6.Certificate.PairSemantics.sound2780 line 1334
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2781 line 1369
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2781 line 1375
90. theorem OAI.MUB6.Certificate.PairSemantics.sound2781 line 1377
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2782 line 1412
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2782 line 1418
93. theorem OAI.MUB6.Certificate.PairSemantics.sound2782 line 1420
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2783 line 1455
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2783 line 1461
96. theorem OAI.MUB6.Certificate.PairSemantics.sound2783 line 1463
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2784 line 1498
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2784 line 1504
99. theorem OAI.MUB6.Certificate.PairSemantics.sound2784 line 1506
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2785 line 1541
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2785 line 1547
102. theorem OAI.MUB6.Certificate.PairSemantics.sound2785 line 1549
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2786 line 1584
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2786 line 1590
105. theorem OAI.MUB6.Certificate.PairSemantics.sound2786 line 1592
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2787 line 1627
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2787 line 1633
108. theorem OAI.MUB6.Certificate.PairSemantics.sound2787 line 1635
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2788 line 1675
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2788 line 1681
111. theorem OAI.MUB6.Certificate.PairSemantics.sound2788 line 1683
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2789 line 1723
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2789 line 1729
114. theorem OAI.MUB6.Certificate.PairSemantics.sound2789 line 1731
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2790 line 1771
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2790 line 1777
117. theorem OAI.MUB6.Certificate.PairSemantics.sound2790 line 1779
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2791 line 1819
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2791 line 1825
120. theorem OAI.MUB6.Certificate.PairSemantics.sound2791 line 1827
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2792 line 1867
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2792 line 1873
123. theorem OAI.MUB6.Certificate.PairSemantics.sound2792 line 1875
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2793 line 1915
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2793 line 1921
126. theorem OAI.MUB6.Certificate.PairSemantics.sound2793 line 1923
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2794 line 1963
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2794 line 1969
129. theorem OAI.MUB6.Certificate.PairSemantics.sound2794 line 1971
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2795 line 2011
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2795 line 2017
132. theorem OAI.MUB6.Certificate.PairSemantics.sound2795 line 2019
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2796 line 2059
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2796 line 2065
135. theorem OAI.MUB6.Certificate.PairSemantics.sound2796 line 2067
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2797 line 2107
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2797 line 2113
138. theorem OAI.MUB6.Certificate.PairSemantics.sound2797 line 2115
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2798 line 2155
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2798 line 2161
141. theorem OAI.MUB6.Certificate.PairSemantics.sound2798 line 2163
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2799 line 2203
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2799 line 2209
144. theorem OAI.MUB6.Certificate.PairSemantics.sound2799 line 2211
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2800 line 2251
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2800 line 2257
147. theorem OAI.MUB6.Certificate.PairSemantics.sound2800 line 2259
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2801 line 2299
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2801 line 2305
150. theorem OAI.MUB6.Certificate.PairSemantics.sound2801 line 2307
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2802 line 2347
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2802 line 2353
153. theorem OAI.MUB6.Certificate.PairSemantics.sound2802 line 2355
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2803 line 2390
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2803 line 2396
156. theorem OAI.MUB6.Certificate.PairSemantics.sound2803 line 2398
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2804 line 2433
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2804 line 2439
159. theorem OAI.MUB6.Certificate.PairSemantics.sound2804 line 2441
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2805 line 2476
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2805 line 2482
162. theorem OAI.MUB6.Certificate.PairSemantics.sound2805 line 2484
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2806 line 2519
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2806 line 2525
165. theorem OAI.MUB6.Certificate.PairSemantics.sound2806 line 2527
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2807 line 2562
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2807 line 2568
168. theorem OAI.MUB6.Certificate.PairSemantics.sound2807 line 2570
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2808 line 2605
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2808 line 2611
171. theorem OAI.MUB6.Certificate.PairSemantics.sound2808 line 2613
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2809 line 2648
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2809 line 2654
174. theorem OAI.MUB6.Certificate.PairSemantics.sound2809 line 2656
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2810 line 2691
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2810 line 2697
177. theorem OAI.MUB6.Certificate.PairSemantics.sound2810 line 2699
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2811 line 2734
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2811 line 2740
180. theorem OAI.MUB6.Certificate.PairSemantics.sound2811 line 2742
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2812 line 2777
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2812 line 2783
183. theorem OAI.MUB6.Certificate.PairSemantics.sound2812 line 2785
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2813 line 2820
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2813 line 2826
186. theorem OAI.MUB6.Certificate.PairSemantics.sound2813 line 2828
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2814 line 2863
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2814 line 2869
189. theorem OAI.MUB6.Certificate.PairSemantics.sound2814 line 2871
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2815 line 2906
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2815 line 2912
192. theorem OAI.MUB6.Certificate.PairSemantics.sound2815 line 2914