mathlib

f900513a - feat(linear_algebra/matrix): slightly generalize `smul_left_mul_matrix` (#7632)

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)