OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound44.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2816 line 100
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2816 line 106
3. theorem OAI.MUB6.Certificate.PairSemantics.sound2816 line 108
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2817 line 143
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2817 line 149
6. theorem OAI.MUB6.Certificate.PairSemantics.sound2817 line 151
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2818 line 186
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2818 line 192
9. theorem OAI.MUB6.Certificate.PairSemantics.sound2818 line 194
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2819 line 229
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2819 line 235
12. theorem OAI.MUB6.Certificate.PairSemantics.sound2819 line 237
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2820 line 272
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2820 line 278
15. theorem OAI.MUB6.Certificate.PairSemantics.sound2820 line 280
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2821 line 315
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2821 line 321
18. theorem OAI.MUB6.Certificate.PairSemantics.sound2821 line 323
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2822 line 358
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2822 line 364
21. theorem OAI.MUB6.Certificate.PairSemantics.sound2822 line 366
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2823 line 401
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2823 line 407
24. theorem OAI.MUB6.Certificate.PairSemantics.sound2823 line 409
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2824 line 444
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2824 line 450
27. theorem OAI.MUB6.Certificate.PairSemantics.sound2824 line 452
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2825 line 487
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2825 line 493
30. theorem OAI.MUB6.Certificate.PairSemantics.sound2825 line 495
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2826 line 530
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2826 line 536
33. theorem OAI.MUB6.Certificate.PairSemantics.sound2826 line 538
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2827 line 573
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2827 line 579
36. theorem OAI.MUB6.Certificate.PairSemantics.sound2827 line 581
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2828 line 616
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2828 line 622
39. theorem OAI.MUB6.Certificate.PairSemantics.sound2828 line 624
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2829 line 659
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2829 line 665
42. theorem OAI.MUB6.Certificate.PairSemantics.sound2829 line 667
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2830 line 702
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2830 line 708
45. theorem OAI.MUB6.Certificate.PairSemantics.sound2830 line 710
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2831 line 745
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2831 line 751
48. theorem OAI.MUB6.Certificate.PairSemantics.sound2831 line 753
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2832 line 788
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2832 line 794
51. theorem OAI.MUB6.Certificate.PairSemantics.sound2832 line 796
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2833 line 831
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2833 line 837
54. theorem OAI.MUB6.Certificate.PairSemantics.sound2833 line 839
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2834 line 874
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2834 line 880
57. theorem OAI.MUB6.Certificate.PairSemantics.sound2834 line 882
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2835 line 917
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2835 line 923
60. theorem OAI.MUB6.Certificate.PairSemantics.sound2835 line 925
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2836 line 960
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2836 line 966
63. theorem OAI.MUB6.Certificate.PairSemantics.sound2836 line 968
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2837 line 1003
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2837 line 1009
66. theorem OAI.MUB6.Certificate.PairSemantics.sound2837 line 1011
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2838 line 1046
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2838 line 1052
69. theorem OAI.MUB6.Certificate.PairSemantics.sound2838 line 1054
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2839 line 1089
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2839 line 1095
72. theorem OAI.MUB6.Certificate.PairSemantics.sound2839 line 1097
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2840 line 1132
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2840 line 1138
75. theorem OAI.MUB6.Certificate.PairSemantics.sound2840 line 1140
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2841 line 1175
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2841 line 1181
78. theorem OAI.MUB6.Certificate.PairSemantics.sound2841 line 1183
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2842 line 1218
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2842 line 1224
81. theorem OAI.MUB6.Certificate.PairSemantics.sound2842 line 1226
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2843 line 1261
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2843 line 1267
84. theorem OAI.MUB6.Certificate.PairSemantics.sound2843 line 1269
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2844 line 1304
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2844 line 1310
87. theorem OAI.MUB6.Certificate.PairSemantics.sound2844 line 1312
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2845 line 1347
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2845 line 1353
90. theorem OAI.MUB6.Certificate.PairSemantics.sound2845 line 1355
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2846 line 1390
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2846 line 1396
93. theorem OAI.MUB6.Certificate.PairSemantics.sound2846 line 1398
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2847 line 1433
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2847 line 1439
96. theorem OAI.MUB6.Certificate.PairSemantics.sound2847 line 1441
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2848 line 1476
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2848 line 1482
99. theorem OAI.MUB6.Certificate.PairSemantics.sound2848 line 1484
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2849 line 1519
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2849 line 1525
102. theorem OAI.MUB6.Certificate.PairSemantics.sound2849 line 1527
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2850 line 1562
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2850 line 1568
105. theorem OAI.MUB6.Certificate.PairSemantics.sound2850 line 1570
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2851 line 1605
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2851 line 1611
108. theorem OAI.MUB6.Certificate.PairSemantics.sound2851 line 1613
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2852 line 1648
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2852 line 1654
111. theorem OAI.MUB6.Certificate.PairSemantics.sound2852 line 1656
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2853 line 1691
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2853 line 1697
114. theorem OAI.MUB6.Certificate.PairSemantics.sound2853 line 1699
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2854 line 1734
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2854 line 1740
117. theorem OAI.MUB6.Certificate.PairSemantics.sound2854 line 1742
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2855 line 1777
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2855 line 1783
120. theorem OAI.MUB6.Certificate.PairSemantics.sound2855 line 1785
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2856 line 1820
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2856 line 1826
123. theorem OAI.MUB6.Certificate.PairSemantics.sound2856 line 1828
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2857 line 1863
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2857 line 1869
126. theorem OAI.MUB6.Certificate.PairSemantics.sound2857 line 1871
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2858 line 1906
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2858 line 1912
129. theorem OAI.MUB6.Certificate.PairSemantics.sound2858 line 1914
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2859 line 1949
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2859 line 1955
132. theorem OAI.MUB6.Certificate.PairSemantics.sound2859 line 1957
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2860 line 1992
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2860 line 1998
135. theorem OAI.MUB6.Certificate.PairSemantics.sound2860 line 2000
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2861 line 2035
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2861 line 2041
138. theorem OAI.MUB6.Certificate.PairSemantics.sound2861 line 2043
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2862 line 2078
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2862 line 2084
141. theorem OAI.MUB6.Certificate.PairSemantics.sound2862 line 2086
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2863 line 2121
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2863 line 2127
144. theorem OAI.MUB6.Certificate.PairSemantics.sound2863 line 2129
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2864 line 2169
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2864 line 2175
147. theorem OAI.MUB6.Certificate.PairSemantics.sound2864 line 2177
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2865 line 2217
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2865 line 2223
150. theorem OAI.MUB6.Certificate.PairSemantics.sound2865 line 2225
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2866 line 2265
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2866 line 2271
153. theorem OAI.MUB6.Certificate.PairSemantics.sound2866 line 2273
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2867 line 2313
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2867 line 2319
156. theorem OAI.MUB6.Certificate.PairSemantics.sound2867 line 2321
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2868 line 2361
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2868 line 2367
159. theorem OAI.MUB6.Certificate.PairSemantics.sound2868 line 2369
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2869 line 2409
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2869 line 2415
162. theorem OAI.MUB6.Certificate.PairSemantics.sound2869 line 2417
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2870 line 2457
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2870 line 2463
165. theorem OAI.MUB6.Certificate.PairSemantics.sound2870 line 2465
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2871 line 2505
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2871 line 2511
168. theorem OAI.MUB6.Certificate.PairSemantics.sound2871 line 2513
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2872 line 2553
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2872 line 2559
171. theorem OAI.MUB6.Certificate.PairSemantics.sound2872 line 2561
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2873 line 2601
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2873 line 2607
174. theorem OAI.MUB6.Certificate.PairSemantics.sound2873 line 2609
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2874 line 2649
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2874 line 2655
177. theorem OAI.MUB6.Certificate.PairSemantics.sound2874 line 2657
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2875 line 2697
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2875 line 2703
180. theorem OAI.MUB6.Certificate.PairSemantics.sound2875 line 2705
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2876 line 2745
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2876 line 2751
183. theorem OAI.MUB6.Certificate.PairSemantics.sound2876 line 2753
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2877 line 2793
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2877 line 2799
186. theorem OAI.MUB6.Certificate.PairSemantics.sound2877 line 2801
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2878 line 2841
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2878 line 2847
189. theorem OAI.MUB6.Certificate.PairSemantics.sound2878 line 2849
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2879 line 2889
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2879 line 2895
192. theorem OAI.MUB6.Certificate.PairSemantics.sound2879 line 2897