OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound42.lean

GitHub source file

192 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2688 line 88
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2688 line 94
3. theorem OAI.MUB6.Certificate.PairSemantics.sound2688 line 96
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2689 line 131
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2689 line 137
6. theorem OAI.MUB6.Certificate.PairSemantics.sound2689 line 139
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2690 line 174
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2690 line 180
9. theorem OAI.MUB6.Certificate.PairSemantics.sound2690 line 182
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2691 line 217
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2691 line 223
12. theorem OAI.MUB6.Certificate.PairSemantics.sound2691 line 225
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2692 line 260
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2692 line 266
15. theorem OAI.MUB6.Certificate.PairSemantics.sound2692 line 268
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2693 line 303
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2693 line 309
18. theorem OAI.MUB6.Certificate.PairSemantics.sound2693 line 311
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2694 line 346
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2694 line 352
21. theorem OAI.MUB6.Certificate.PairSemantics.sound2694 line 354
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2695 line 389
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2695 line 395
24. theorem OAI.MUB6.Certificate.PairSemantics.sound2695 line 397
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2696 line 432
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2696 line 438
27. theorem OAI.MUB6.Certificate.PairSemantics.sound2696 line 440
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2697 line 475
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2697 line 481
30. theorem OAI.MUB6.Certificate.PairSemantics.sound2697 line 483
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2698 line 518
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2698 line 524
33. theorem OAI.MUB6.Certificate.PairSemantics.sound2698 line 526
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2699 line 561
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2699 line 567
36. theorem OAI.MUB6.Certificate.PairSemantics.sound2699 line 569
37. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2700 line 604
38. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2700 line 610
39. theorem OAI.MUB6.Certificate.PairSemantics.sound2700 line 612
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2701 line 647
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2701 line 653
42. theorem OAI.MUB6.Certificate.PairSemantics.sound2701 line 655
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2702 line 690
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2702 line 696
45. theorem OAI.MUB6.Certificate.PairSemantics.sound2702 line 698
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2703 line 733
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2703 line 739
48. theorem OAI.MUB6.Certificate.PairSemantics.sound2703 line 741
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2704 line 776
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2704 line 782
51. theorem OAI.MUB6.Certificate.PairSemantics.sound2704 line 784
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2705 line 819
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2705 line 825
54. theorem OAI.MUB6.Certificate.PairSemantics.sound2705 line 827
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2706 line 862
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2706 line 868
57. theorem OAI.MUB6.Certificate.PairSemantics.sound2706 line 870
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2707 line 905
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2707 line 911
60. theorem OAI.MUB6.Certificate.PairSemantics.sound2707 line 913
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2708 line 948
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2708 line 954
63. theorem OAI.MUB6.Certificate.PairSemantics.sound2708 line 956
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2709 line 991
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2709 line 997
66. theorem OAI.MUB6.Certificate.PairSemantics.sound2709 line 999
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2710 line 1034
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2710 line 1040
69. theorem OAI.MUB6.Certificate.PairSemantics.sound2710 line 1042
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2711 line 1077
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2711 line 1083
72. theorem OAI.MUB6.Certificate.PairSemantics.sound2711 line 1085
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2712 line 1120
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2712 line 1126
75. theorem OAI.MUB6.Certificate.PairSemantics.sound2712 line 1128
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2713 line 1163
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2713 line 1169
78. theorem OAI.MUB6.Certificate.PairSemantics.sound2713 line 1171
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2714 line 1206
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2714 line 1212
81. theorem OAI.MUB6.Certificate.PairSemantics.sound2714 line 1214
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2715 line 1249
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2715 line 1255
84. theorem OAI.MUB6.Certificate.PairSemantics.sound2715 line 1257
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2716 line 1292
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2716 line 1298
87. theorem OAI.MUB6.Certificate.PairSemantics.sound2716 line 1300
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2717 line 1335
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2717 line 1341
90. theorem OAI.MUB6.Certificate.PairSemantics.sound2717 line 1343
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2718 line 1378
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2718 line 1384
93. theorem OAI.MUB6.Certificate.PairSemantics.sound2718 line 1386
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2719 line 1421
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2719 line 1427
96. theorem OAI.MUB6.Certificate.PairSemantics.sound2719 line 1429
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2720 line 1464
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2720 line 1470
99. theorem OAI.MUB6.Certificate.PairSemantics.sound2720 line 1472
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2721 line 1507
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2721 line 1513
102. theorem OAI.MUB6.Certificate.PairSemantics.sound2721 line 1515
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2722 line 1550
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2722 line 1556
105. theorem OAI.MUB6.Certificate.PairSemantics.sound2722 line 1558
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2723 line 1593
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2723 line 1599
108. theorem OAI.MUB6.Certificate.PairSemantics.sound2723 line 1601
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2724 line 1636
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2724 line 1642
111. theorem OAI.MUB6.Certificate.PairSemantics.sound2724 line 1644
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2725 line 1679
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2725 line 1685
114. theorem OAI.MUB6.Certificate.PairSemantics.sound2725 line 1687
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2726 line 1722
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2726 line 1728
117. theorem OAI.MUB6.Certificate.PairSemantics.sound2726 line 1730
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2727 line 1765
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2727 line 1771
120. theorem OAI.MUB6.Certificate.PairSemantics.sound2727 line 1773
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2728 line 1808
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2728 line 1814
123. theorem OAI.MUB6.Certificate.PairSemantics.sound2728 line 1816
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2729 line 1851
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2729 line 1857
126. theorem OAI.MUB6.Certificate.PairSemantics.sound2729 line 1859
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2730 line 1894
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2730 line 1900
129. theorem OAI.MUB6.Certificate.PairSemantics.sound2730 line 1902
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2731 line 1937
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2731 line 1943
132. theorem OAI.MUB6.Certificate.PairSemantics.sound2731 line 1945
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2732 line 1980
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2732 line 1986
135. theorem OAI.MUB6.Certificate.PairSemantics.sound2732 line 1988
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2733 line 2023
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2733 line 2029
138. theorem OAI.MUB6.Certificate.PairSemantics.sound2733 line 2031
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2734 line 2066
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2734 line 2072
141. theorem OAI.MUB6.Certificate.PairSemantics.sound2734 line 2074
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2735 line 2109
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2735 line 2115
144. theorem OAI.MUB6.Certificate.PairSemantics.sound2735 line 2117
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2736 line 2152
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2736 line 2158
147. theorem OAI.MUB6.Certificate.PairSemantics.sound2736 line 2160
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2737 line 2195
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2737 line 2201
150. theorem OAI.MUB6.Certificate.PairSemantics.sound2737 line 2203
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2738 line 2238
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2738 line 2244
153. theorem OAI.MUB6.Certificate.PairSemantics.sound2738 line 2246
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2739 line 2281
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2739 line 2287
156. theorem OAI.MUB6.Certificate.PairSemantics.sound2739 line 2289
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2740 line 2324
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2740 line 2330
159. theorem OAI.MUB6.Certificate.PairSemantics.sound2740 line 2332
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2741 line 2367
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2741 line 2373
162. theorem OAI.MUB6.Certificate.PairSemantics.sound2741 line 2375
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2742 line 2410
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2742 line 2416
165. theorem OAI.MUB6.Certificate.PairSemantics.sound2742 line 2418
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2743 line 2453
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2743 line 2459
168. theorem OAI.MUB6.Certificate.PairSemantics.sound2743 line 2461
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2744 line 2496
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2744 line 2502
171. theorem OAI.MUB6.Certificate.PairSemantics.sound2744 line 2504
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2745 line 2539
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2745 line 2545
174. theorem OAI.MUB6.Certificate.PairSemantics.sound2745 line 2547
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2746 line 2582
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2746 line 2588
177. theorem OAI.MUB6.Certificate.PairSemantics.sound2746 line 2590
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2747 line 2625
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2747 line 2631
180. theorem OAI.MUB6.Certificate.PairSemantics.sound2747 line 2633
181. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2748 line 2668
182. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2748 line 2674
183. theorem OAI.MUB6.Certificate.PairSemantics.sound2748 line 2676
184. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2749 line 2711
185. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2749 line 2717
186. theorem OAI.MUB6.Certificate.PairSemantics.sound2749 line 2719
187. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2750 line 2754
188. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2750 line 2760
189. theorem OAI.MUB6.Certificate.PairSemantics.sound2750 line 2762
190. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation2751 line 2797
191. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix2751 line 2803
192. theorem OAI.MUB6.Certificate.PairSemantics.sound2751 line 2805