mathlib3

820b2296 - feat(data/matrix/reflection): add `mul_vec` and `vec_mul` (#18805)

feat(data/matrix/reflection): add `mul_vec` and `vec_mul` (#18805) This follows the pattern already established by `mul`. The motivation was an example on Zulip which wanted to compute the product of ```lean def M := !![(2:ℂ), 0, 0; 0, 1, 0; 0, 0, 1] def v := ![(0:ℂ), 0, 1] ``` As before, the meta code that makes this pleasant to use is absent, but I will add it along with the rest of the meta code in #15738.