OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound11.lean

GitHub source file

180 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation704 line 64
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix704 line 70
3. theorem OAI.MUB6.Certificate.PairSemantics.sound704 line 72
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation705 line 107
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix705 line 113
6. theorem OAI.MUB6.Certificate.PairSemantics.sound705 line 115
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation706 line 150
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix706 line 156
9. theorem OAI.MUB6.Certificate.PairSemantics.sound706 line 158
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation707 line 193
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix707 line 199
12. theorem OAI.MUB6.Certificate.PairSemantics.sound707 line 201
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation708 line 236
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix708 line 242
15. theorem OAI.MUB6.Certificate.PairSemantics.sound708 line 244
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation709 line 279
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix709 line 285
18. theorem OAI.MUB6.Certificate.PairSemantics.sound709 line 287
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation710 line 322
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix710 line 328
21. theorem OAI.MUB6.Certificate.PairSemantics.sound710 line 330
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation711 line 365
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix711 line 371
24. theorem OAI.MUB6.Certificate.PairSemantics.sound711 line 373
25. theorem OAI.MUB6.Certificate.PairSemantics.sound712 line 408
26. theorem OAI.MUB6.Certificate.PairSemantics.sound713 line 413
27. theorem OAI.MUB6.Certificate.PairSemantics.sound714 line 418
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation715 line 423
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix715 line 429
30. theorem OAI.MUB6.Certificate.PairSemantics.sound715 line 431
31. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation716 line 471
32. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix716 line 477
33. theorem OAI.MUB6.Certificate.PairSemantics.sound716 line 479
34. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation717 line 519
35. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix717 line 525
36. theorem OAI.MUB6.Certificate.PairSemantics.sound717 line 527
37. theorem OAI.MUB6.Certificate.PairSemantics.sound718 line 567
38. theorem OAI.MUB6.Certificate.PairSemantics.sound719 line 572
39. theorem OAI.MUB6.Certificate.PairSemantics.sound720 line 577
40. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation721 line 582
41. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix721 line 588
42. theorem OAI.MUB6.Certificate.PairSemantics.sound721 line 590
43. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation722 line 625
44. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix722 line 631
45. theorem OAI.MUB6.Certificate.PairSemantics.sound722 line 633
46. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation723 line 668
47. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix723 line 674
48. theorem OAI.MUB6.Certificate.PairSemantics.sound723 line 676
49. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation724 line 711
50. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix724 line 717
51. theorem OAI.MUB6.Certificate.PairSemantics.sound724 line 719
52. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation725 line 754
53. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix725 line 760
54. theorem OAI.MUB6.Certificate.PairSemantics.sound725 line 762
55. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation726 line 793
56. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix726 line 799
57. theorem OAI.MUB6.Certificate.PairSemantics.sound726 line 801
58. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation727 line 832
59. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix727 line 838
60. theorem OAI.MUB6.Certificate.PairSemantics.sound727 line 840
61. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation728 line 871
62. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix728 line 877
63. theorem OAI.MUB6.Certificate.PairSemantics.sound728 line 879
64. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation729 line 910
65. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix729 line 916
66. theorem OAI.MUB6.Certificate.PairSemantics.sound729 line 918
67. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation730 line 949
68. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix730 line 955
69. theorem OAI.MUB6.Certificate.PairSemantics.sound730 line 957
70. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation731 line 988
71. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix731 line 994
72. theorem OAI.MUB6.Certificate.PairSemantics.sound731 line 996
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation732 line 1027
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix732 line 1033
75. theorem OAI.MUB6.Certificate.PairSemantics.sound732 line 1035
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation733 line 1070
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix733 line 1076
78. theorem OAI.MUB6.Certificate.PairSemantics.sound733 line 1078
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation734 line 1113
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix734 line 1119
81. theorem OAI.MUB6.Certificate.PairSemantics.sound734 line 1121
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation735 line 1156
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix735 line 1162
84. theorem OAI.MUB6.Certificate.PairSemantics.sound735 line 1164
85. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation736 line 1199
86. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix736 line 1205
87. theorem OAI.MUB6.Certificate.PairSemantics.sound736 line 1207
88. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation737 line 1242
89. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix737 line 1248
90. theorem OAI.MUB6.Certificate.PairSemantics.sound737 line 1250
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation738 line 1285
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix738 line 1291
93. theorem OAI.MUB6.Certificate.PairSemantics.sound738 line 1293
94. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation739 line 1328
95. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix739 line 1334
96. theorem OAI.MUB6.Certificate.PairSemantics.sound739 line 1336
97. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation740 line 1371
98. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix740 line 1377
99. theorem OAI.MUB6.Certificate.PairSemantics.sound740 line 1379
100. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation741 line 1414
101. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix741 line 1420
102. theorem OAI.MUB6.Certificate.PairSemantics.sound741 line 1422
103. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation742 line 1457
104. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix742 line 1463
105. theorem OAI.MUB6.Certificate.PairSemantics.sound742 line 1465
106. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation743 line 1500
107. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix743 line 1506
108. theorem OAI.MUB6.Certificate.PairSemantics.sound743 line 1508
109. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation744 line 1543
110. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix744 line 1549
111. theorem OAI.MUB6.Certificate.PairSemantics.sound744 line 1551
112. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation745 line 1586
113. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix745 line 1592
114. theorem OAI.MUB6.Certificate.PairSemantics.sound745 line 1594
115. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation746 line 1629
116. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix746 line 1635
117. theorem OAI.MUB6.Certificate.PairSemantics.sound746 line 1637
118. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation747 line 1672
119. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix747 line 1678
120. theorem OAI.MUB6.Certificate.PairSemantics.sound747 line 1680
121. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation748 line 1715
122. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix748 line 1721
123. theorem OAI.MUB6.Certificate.PairSemantics.sound748 line 1723
124. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation749 line 1758
125. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix749 line 1764
126. theorem OAI.MUB6.Certificate.PairSemantics.sound749 line 1766
127. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation750 line 1801
128. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix750 line 1807
129. theorem OAI.MUB6.Certificate.PairSemantics.sound750 line 1809
130. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation751 line 1839
131. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix751 line 1845
132. theorem OAI.MUB6.Certificate.PairSemantics.sound751 line 1847
133. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation752 line 1877
134. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix752 line 1883
135. theorem OAI.MUB6.Certificate.PairSemantics.sound752 line 1885
136. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation753 line 1916
137. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix753 line 1922
138. theorem OAI.MUB6.Certificate.PairSemantics.sound753 line 1924
139. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation754 line 1955
140. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix754 line 1961
141. theorem OAI.MUB6.Certificate.PairSemantics.sound754 line 1963
142. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation755 line 1993
143. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix755 line 1999
144. theorem OAI.MUB6.Certificate.PairSemantics.sound755 line 2001
145. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation756 line 2031
146. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix756 line 2037
147. theorem OAI.MUB6.Certificate.PairSemantics.sound756 line 2039
148. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation757 line 2070
149. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix757 line 2076
150. theorem OAI.MUB6.Certificate.PairSemantics.sound757 line 2078
151. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation758 line 2109
152. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix758 line 2115
153. theorem OAI.MUB6.Certificate.PairSemantics.sound758 line 2117
154. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation759 line 2148
155. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix759 line 2154
156. theorem OAI.MUB6.Certificate.PairSemantics.sound759 line 2156
157. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation760 line 2187
158. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix760 line 2193
159. theorem OAI.MUB6.Certificate.PairSemantics.sound760 line 2195
160. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation761 line 2225
161. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix761 line 2231
162. theorem OAI.MUB6.Certificate.PairSemantics.sound761 line 2233
163. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation762 line 2263
164. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix762 line 2269
165. theorem OAI.MUB6.Certificate.PairSemantics.sound762 line 2271
166. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation763 line 2301
167. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix763 line 2307
168. theorem OAI.MUB6.Certificate.PairSemantics.sound763 line 2309
169. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation764 line 2339
170. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix764 line 2345
171. theorem OAI.MUB6.Certificate.PairSemantics.sound764 line 2347
172. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation765 line 2377
173. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix765 line 2383
174. theorem OAI.MUB6.Certificate.PairSemantics.sound765 line 2385
175. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation766 line 2415
176. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix766 line 2421
177. theorem OAI.MUB6.Certificate.PairSemantics.sound766 line 2423
178. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation767 line 2453
179. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix767 line 2459
180. theorem OAI.MUB6.Certificate.PairSemantics.sound767 line 2461