OAI/Analysis/MutuallyUnbiased/PairSemantics/Sound1.lean

GitHub source file

152 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation64 line 43
2. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix64 line 49
3. theorem OAI.MUB6.Certificate.PairSemantics.sound64 line 51
4. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation65 line 76
5. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix65 line 82
6. theorem OAI.MUB6.Certificate.PairSemantics.sound65 line 84
7. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation66 line 114
8. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix66 line 120
9. theorem OAI.MUB6.Certificate.PairSemantics.sound66 line 122
10. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation67 line 157
11. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix67 line 163
12. theorem OAI.MUB6.Certificate.PairSemantics.sound67 line 165
13. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation68 line 200
14. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix68 line 206
15. theorem OAI.MUB6.Certificate.PairSemantics.sound68 line 208
16. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation69 line 243
17. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix69 line 249
18. theorem OAI.MUB6.Certificate.PairSemantics.sound69 line 251
19. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation70 line 286
20. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix70 line 292
21. theorem OAI.MUB6.Certificate.PairSemantics.sound70 line 294
22. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation71 line 324
23. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix71 line 330
24. theorem OAI.MUB6.Certificate.PairSemantics.sound71 line 332
25. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation72 line 362
26. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix72 line 368
27. theorem OAI.MUB6.Certificate.PairSemantics.sound72 line 370
28. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation73 line 400
29. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix73 line 406
30. theorem OAI.MUB6.Certificate.PairSemantics.sound73 line 408
31. theorem OAI.MUB6.Certificate.PairSemantics.sound74 line 438
32. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation75 line 443
33. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix75 line 449
34. theorem OAI.MUB6.Certificate.PairSemantics.sound75 line 451
35. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation76 line 481
36. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix76 line 487
37. theorem OAI.MUB6.Certificate.PairSemantics.sound76 line 489
38. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation77 line 519
39. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix77 line 525
40. theorem OAI.MUB6.Certificate.PairSemantics.sound77 line 527
41. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation78 line 557
42. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix78 line 563
43. theorem OAI.MUB6.Certificate.PairSemantics.sound78 line 565
44. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation79 line 595
45. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix79 line 601
46. theorem OAI.MUB6.Certificate.PairSemantics.sound79 line 603
47. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation80 line 633
48. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix80 line 639
49. theorem OAI.MUB6.Certificate.PairSemantics.sound80 line 641
50. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation81 line 671
51. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix81 line 677
52. theorem OAI.MUB6.Certificate.PairSemantics.sound81 line 679
53. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation82 line 709
54. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix82 line 715
55. theorem OAI.MUB6.Certificate.PairSemantics.sound82 line 717
56. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation83 line 747
57. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix83 line 753
58. theorem OAI.MUB6.Certificate.PairSemantics.sound83 line 755
59. theorem OAI.MUB6.Certificate.PairSemantics.sound84 line 785
60. theorem OAI.MUB6.Certificate.PairSemantics.sound85 line 790
61. theorem OAI.MUB6.Certificate.PairSemantics.sound86 line 795
62. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation87 line 800
63. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix87 line 806
64. theorem OAI.MUB6.Certificate.PairSemantics.sound87 line 808
65. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation88 line 838
66. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix88 line 844
67. theorem OAI.MUB6.Certificate.PairSemantics.sound88 line 846
68. theorem OAI.MUB6.Certificate.PairSemantics.sound89 line 876
69. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation90 line 881
70. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix90 line 887
71. theorem OAI.MUB6.Certificate.PairSemantics.sound90 line 889
72. theorem OAI.MUB6.Certificate.PairSemantics.sound91 line 919
73. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation92 line 924
74. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix92 line 930
75. theorem OAI.MUB6.Certificate.PairSemantics.sound92 line 932
76. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation93 line 962
77. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix93 line 968
78. theorem OAI.MUB6.Certificate.PairSemantics.sound93 line 970
79. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation94 line 1000
80. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix94 line 1006
81. theorem OAI.MUB6.Certificate.PairSemantics.sound94 line 1008
82. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation95 line 1038
83. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix95 line 1044
84. theorem OAI.MUB6.Certificate.PairSemantics.sound95 line 1046
85. theorem OAI.MUB6.Certificate.PairSemantics.sound96 line 1076
86. theorem OAI.MUB6.Certificate.PairSemantics.sound97 line 1081
87. theorem OAI.MUB6.Certificate.PairSemantics.sound98 line 1086
88. theorem OAI.MUB6.Certificate.PairSemantics.sound99 line 1091
89. theorem OAI.MUB6.Certificate.PairSemantics.sound100 line 1096
90. theorem OAI.MUB6.Certificate.PairSemantics.sound101 line 1101
91. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation102 line 1106
92. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix102 line 1112
93. theorem OAI.MUB6.Certificate.PairSemantics.sound102 line 1114
94. theorem OAI.MUB6.Certificate.PairSemantics.sound103 line 1144
95. theorem OAI.MUB6.Certificate.PairSemantics.sound104 line 1149
96. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation105 line 1154
97. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix105 line 1160
98. theorem OAI.MUB6.Certificate.PairSemantics.sound105 line 1162
99. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation106 line 1192
100. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix106 line 1198
101. theorem OAI.MUB6.Certificate.PairSemantics.sound106 line 1200
102. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation107 line 1230
103. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix107 line 1236
104. theorem OAI.MUB6.Certificate.PairSemantics.sound107 line 1238
105. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation108 line 1268
106. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix108 line 1274
107. theorem OAI.MUB6.Certificate.PairSemantics.sound108 line 1276
108. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation109 line 1306
109. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix109 line 1312
110. theorem OAI.MUB6.Certificate.PairSemantics.sound109 line 1314
111. theorem OAI.MUB6.Certificate.PairSemantics.sound110 line 1344
112. theorem OAI.MUB6.Certificate.PairSemantics.sound111 line 1349
113. theorem OAI.MUB6.Certificate.PairSemantics.sound112 line 1354
114. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation113 line 1359
115. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix113 line 1365
116. theorem OAI.MUB6.Certificate.PairSemantics.sound113 line 1367
117. theorem OAI.MUB6.Certificate.PairSemantics.sound114 line 1397
118. theorem OAI.MUB6.Certificate.PairSemantics.sound115 line 1402
119. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation116 line 1407
120. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix116 line 1413
121. theorem OAI.MUB6.Certificate.PairSemantics.sound116 line 1415
122. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation117 line 1450
123. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix117 line 1456
124. theorem OAI.MUB6.Certificate.PairSemantics.sound117 line 1458
125. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation118 line 1493
126. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix118 line 1499
127. theorem OAI.MUB6.Certificate.PairSemantics.sound118 line 1501
128. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation119 line 1536
129. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix119 line 1542
130. theorem OAI.MUB6.Certificate.PairSemantics.sound119 line 1544
131. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation120 line 1574
132. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix120 line 1580
133. theorem OAI.MUB6.Certificate.PairSemantics.sound120 line 1582
134. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation121 line 1612
135. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix121 line 1618
136. theorem OAI.MUB6.Certificate.PairSemantics.sound121 line 1620
137. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation122 line 1650
138. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix122 line 1656
139. theorem OAI.MUB6.Certificate.PairSemantics.sound122 line 1658
140. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation123 line 1688
141. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix123 line 1694
142. theorem OAI.MUB6.Certificate.PairSemantics.sound123 line 1696
143. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation124 line 1726
144. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix124 line 1732
145. theorem OAI.MUB6.Certificate.PairSemantics.sound124 line 1734
146. theorem OAI.MUB6.Certificate.PairSemantics.sound125 line 1764
147. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation126 line 1769
148. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix126 line 1775
149. theorem OAI.MUB6.Certificate.PairSemantics.sound126 line 1777
150. def OAI.MUB6.Certificate.PairSemantics.pivotPermutation127 line 1807
151. def OAI.MUB6.Certificate.PairSemantics.pivotMatrix127 line 1813
152. theorem OAI.MUB6.Certificate.PairSemantics.sound127 line 1815