OAI/LinearAlgebra/MatrixFields/CapacityA/CapA3_6_7I1.lean

GitHub source file

354 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0Value line 16
2. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0Raw line 17
3. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0Raw_sound line 18
4. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0Certificates line 21
5. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0Certificates_valid line 24
6. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0CertificateIndex line 26
7. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0P line 30
8. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0P_check line 32
9. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0P_sound line 34
10. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0Terms line 37
11. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0Terms_sound line 39
12. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0Entropy line 43
13. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0Entropy_sound line 44
14. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0Mass line 46
15. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0Mass_sound line 47
16. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0MassTermLogWitness line 49
17. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0MassTermLog line 50
18. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0MassTermLog_sound line 51
19. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0MassTerm line 55
20. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0MassTerm_sound line 56
21. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0H line 58
22. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R0H_sound line 59
23. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1Value line 61
24. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1Raw line 62
25. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1Raw_sound line 63
26. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1Certificates line 66
27. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1Certificates_valid line 69
28. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1CertificateIndex line 71
29. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1P line 76
30. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1P_check line 78
31. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1P_sound line 80
32. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1Terms line 83
33. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1Terms_sound line 85
34. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1Entropy line 89
35. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1Entropy_sound line 90
36. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1Mass line 92
37. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1Mass_sound line 93
38. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1MassTermLogWitness line 95
39. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1MassTermLog line 96
40. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1MassTermLog_sound line 97
41. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1MassTerm line 101
42. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1MassTerm_sound line 102
43. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1H line 104
44. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R1H_sound line 105
45. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2Value line 107
46. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2Raw line 108
47. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2Raw_sound line 109
48. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2Certificates line 112
49. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2Certificates_valid line 117
50. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2CertificateIndex line 119
51. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2P line 127
52. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2P_check line 129
53. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2P_sound line 131
54. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2Terms line 134
55. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2Terms_sound line 136
56. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2Entropy line 140
57. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2Entropy_sound line 141
58. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2Mass line 143
59. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2Mass_sound line 144
60. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2MassTermLogWitness line 146
61. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2MassTermLog line 147
62. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2MassTermLog_sound line 148
63. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2MassTerm line 152
64. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2MassTerm_sound line 153
65. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2H line 155
66. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R2H_sound line 156
67. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3Value line 158
68. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3Raw line 159
69. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3Raw_sound line 160
70. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3Certificates line 163
71. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3Certificates_valid line 168
72. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3CertificateIndex line 170
73. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3P line 179
74. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3P_check line 181
75. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3P_sound line 183
76. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3Terms line 186
77. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3Terms_sound line 188
78. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3Entropy line 192
79. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3Entropy_sound line 193
80. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3Mass line 195
81. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3Mass_sound line 196
82. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3MassTermLogWitness line 198
83. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3MassTermLog line 199
84. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3MassTermLog_sound line 200
85. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3MassTerm line 204
86. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3MassTerm_sound line 205
87. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3H line 207
88. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R3H_sound line 208
89. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4Value line 210
90. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4Raw line 211
91. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4Raw_sound line 212
92. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4Certificates line 215
93. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4Certificates_valid line 222
94. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4CertificateIndex line 224
95. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4P line 235
96. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4P_check line 237
97. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4P_sound line 239
98. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4Terms line 242
99. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4Terms_sound line 244
100. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4Entropy line 248
101. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4Entropy_sound line 249
102. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4Mass line 251
103. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4Mass_sound line 252
104. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4MassTermLogWitness line 254
105. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4MassTermLog line 255
106. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4MassTermLog_sound line 256
107. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4MassTerm line 260
108. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4MassTerm_sound line 261
109. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4H line 263
110. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R4H_sound line 264
111. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5Value line 266
112. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5Raw line 267
113. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5Raw_sound line 268
114. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5Certificates line 271
115. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5Certificates_valid line 276
116. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5CertificateIndex line 278
117. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5P line 287
118. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5P_check line 289
119. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5P_sound line 291
120. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5Terms line 294
121. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5Terms_sound line 296
122. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5Entropy line 300
123. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5Entropy_sound line 301
124. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5Mass line 303
125. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5Mass_sound line 304
126. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5MassTermLogWitness line 306
127. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5MassTermLog line 307
128. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5MassTermLog_sound line 308
129. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5MassTerm line 312
130. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5MassTerm_sound line 313
131. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5H line 315
132. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R5H_sound line 316
133. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6Value line 318
134. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6Raw line 319
135. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6Raw_sound line 320
136. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6Certificates line 323
137. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6Certificates_valid line 328
138. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6CertificateIndex line 330
139. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6P line 338
140. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6P_check line 340
141. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6P_sound line 342
142. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6Terms line 345
143. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6Terms_sound line 347
144. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6Entropy line 351
145. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6Entropy_sound line 352
146. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6Mass line 354
147. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6Mass_sound line 355
148. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6MassTermLogWitness line 357
149. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6MassTermLog line 358
150. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6MassTermLog_sound line 359
151. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6MassTerm line 363
152. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6MassTerm_sound line 364
153. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6H line 366
154. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R6H_sound line 367
155. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R7Value line 369
156. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R7Raw line 370
157. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R7Raw_sound line 371
158. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R7Certificates line 374
159. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R7Certificates_valid line 376
160. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R7CertificateIndex line 378
161. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R7P line 381
162. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R7P_check line 383
163. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R7P_sound line 385
164. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R7Terms line 388
165. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R7Terms_sound line 390
166. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R7Entropy line 394
167. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R7Entropy_sound line 395
168. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R7Mass line 397
169. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R7Mass_sound line 398
170. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R7MassTerm line 400
171. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R7MassTerm_sound line 401
172. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R7H line 403
173. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R7H_sound line 404
174. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R8Value line 406
175. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R8Raw line 407
176. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R8Raw_sound line 408
177. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R8Certificates line 411
178. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R8Certificates_valid line 413
179. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R8CertificateIndex line 415
180. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R8P line 418
181. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R8P_check line 420
182. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R8P_sound line 422
183. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R8Terms line 425
184. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R8Terms_sound line 427
185. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R8Entropy line 431
186. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R8Entropy_sound line 432
187. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R8Mass line 434
188. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R8Mass_sound line 435
189. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R8MassTerm line 437
190. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R8MassTerm_sound line 438
191. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R8H line 440
192. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R8H_sound line 441
193. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R9Value line 443
194. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R9Raw line 444
195. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R9Raw_sound line 445
196. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R9Certificates line 448
197. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R9Certificates_valid line 450
198. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R9CertificateIndex line 452
199. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R9P line 455
200. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R9P_check line 457
201. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R9P_sound line 459
202. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R9Terms line 462
203. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R9Terms_sound line 464
204. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R9Entropy line 468
205. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R9Entropy_sound line 469
206. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R9Mass line 471
207. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R9Mass_sound line 472
208. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R9MassTerm line 474
209. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R9MassTerm_sound line 475
210. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R9H line 477
211. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R9H_sound line 478
212. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R10Value line 480
213. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R10Raw line 481
214. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R10Raw_sound line 482
215. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R10Certificates line 485
216. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R10Certificates_valid line 487
217. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R10CertificateIndex line 489
218. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R10P line 492
219. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R10P_check line 494
220. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R10P_sound line 496
221. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R10Terms line 499
222. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R10Terms_sound line 501
223. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R10Entropy line 505
224. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R10Entropy_sound line 506
225. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R10Mass line 508
226. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R10Mass_sound line 509
227. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R10MassTerm line 511
228. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R10MassTerm_sound line 512
229. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R10H line 514
230. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R10H_sound line 515
231. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R11Value line 517
232. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R11Raw line 518
233. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R11Raw_sound line 519
234. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R11Certificates line 522
235. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R11Certificates_valid line 524
236. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R11CertificateIndex line 526
237. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R11P line 529
238. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R11P_check line 531
239. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R11P_sound line 533
240. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R11Terms line 536
241. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R11Terms_sound line 538
242. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R11Entropy line 542
243. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R11Entropy_sound line 543
244. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R11Mass line 545
245. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R11Mass_sound line 546
246. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R11MassTerm line 548
247. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R11MassTerm_sound line 549
248. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R11H line 551
249. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R11H_sound line 552
250. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R12Value line 554
251. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R12Raw line 555
252. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R12Raw_sound line 556
253. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R12Certificates line 559
254. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R12Certificates_valid line 561
255. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R12CertificateIndex line 563
256. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R12P line 566
257. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R12P_check line 568
258. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R12P_sound line 570
259. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R12Terms line 573
260. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R12Terms_sound line 575
261. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R12Entropy line 579
262. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R12Entropy_sound line 580
263. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R12Mass line 582
264. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R12Mass_sound line 583
265. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R12MassTerm line 585
266. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R12MassTerm_sound line 586
267. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R12H line 588
268. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R12H_sound line 589
269. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R13Value line 591
270. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R13Raw line 592
271. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R13Raw_sound line 593
272. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R13Certificates line 596
273. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R13Certificates_valid line 598
274. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R13CertificateIndex line 600
275. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R13P line 603
276. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R13P_check line 605
277. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R13P_sound line 607
278. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R13Terms line 610
279. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R13Terms_sound line 612
280. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R13Entropy line 616
281. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R13Entropy_sound line 617
282. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R13Mass line 619
283. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R13Mass_sound line 620
284. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R13MassTerm line 622
285. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R13MassTerm_sound line 623
286. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R13H line 625
287. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R13H_sound line 626
288. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R14Value line 628
289. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R14Raw line 629
290. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R14Raw_sound line 630
291. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R14Certificates line 633
292. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R14Certificates_valid line 635
293. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R14CertificateIndex line 637
294. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R14P line 640
295. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R14P_check line 642
296. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R14P_sound line 644
297. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R14Terms line 647
298. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R14Terms_sound line 649
299. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R14Entropy line 653
300. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R14Entropy_sound line 654
301. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R14Mass line 656
302. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R14Mass_sound line 657
303. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R14MassTerm line 659
304. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R14MassTerm_sound line 660
305. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R14H line 662
306. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R14H_sound line 663
307. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R15Value line 665
308. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R15Raw line 666
309. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R15Raw_sound line 667
310. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R15Certificates line 670
311. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R15Certificates_valid line 672
312. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R15CertificateIndex line 674
313. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R15P line 677
314. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R15P_check line 679
315. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R15P_sound line 681
316. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R15Terms line 684
317. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R15Terms_sound line 686
318. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R15Entropy line 690
319. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R15Entropy_sound line 691
320. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R15Mass line 693
321. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R15Mass_sound line 694
322. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R15MassTerm line 696
323. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R15MassTerm_sound line 697
324. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R15H line 699
325. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R15H_sound line 700
326. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R16Value line 702
327. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R16Raw line 703
328. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R16Raw_sound line 704
329. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R16Certificates line 707
330. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R16Certificates_valid line 709
331. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R16CertificateIndex line 711
332. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R16P line 714
333. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R16P_check line 716
334. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R16P_sound line 718
335. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R16Terms line 721
336. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R16Terms_sound line 723
337. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R16Entropy line 727
338. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R16Entropy_sound line 728
339. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R16Mass line 730
340. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R16Mass_sound line 731
341. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R16MassTerm line 733
342. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R16MassTerm_sound line 734
343. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R16H line 736
344. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1R16H_sound line 737
345. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1ResidualEntropies line 739
346. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1ResidualEntropies_sound line 759
347. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1Singles line 780
348. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1Singles_sound line 785
349. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1Singleton line 817
350. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1Singleton_sound line 818
351. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1Group line 822
352. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1Group_sound line 823
353. def OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1H line 845
354. lemma OAI.MatrixAllFields.MatrixMultiplication.NativeNumerics.CA3_6_7I1_sound line 846