mathlib3

892f8899 - feat(data/matrix/basic): lemmas about mul_vec and single (#13835)

feat(data/matrix/basic): lemmas about mul_vec and single (#13835) We seem to be proving variants of the same statement over and over again; this introduces a new lemma that we can use to prove all these variants trivially in term mode. The new lemmas are: * `matrix.mul_vec_single` * `matrix.single_vec_mul` * `matrix.diagonal_mul_vec_single` * `matrix.single_vec_mul_diagonal` A lot of the proofs got shorter by avoiding `ext` which invokes a more powerful lemma than we actually need.