mathlib

4ae97924 - chore(data/matrix/basic): add lemmas about dot_product and mul_vec (#8325)

chore(data/matrix/basic): add lemmas about dot_product and mul_vec (#8325) This renames: * `mul_vec_one` to `one_mul_vec` * `mul_vec_zero` to `zero_mul_vec` and adds the new lemmas: * `sub_mul_vec` * `mul_vec_sub` * `zero_mul_vec` * `mul_vec_zero` * `sub_dot_product` * `dot_product_sub` Some existing lemmas have had their variables extracted to sections. Co-authored-by: l534zhan <luming.zhang@merton.ox.ac.uk>