Commit 2021-05-18 02:58 f900513a

feat(linear_algebra/matrix): slightly generalize smul_left_mul_matrix (#7632) Two minor changes that make smul_left_mul_matrix slightly easier to apply:

• the bases b and c can now be indexed by different types
• replace (i, k) on the LHS with ik.1 ik.2 on the RHS (so you don't have to introduce the constructor with rw ← prod.mk.eta somewhere deep in your expression)