Commit 2021-07-16 00:27 4ae97924
View on Github →chore(data/matrix/basic): add lemmas about dot_product and mul_vec (#8325) This renames:
mul_vec_one
toone_mul_vec
mul_vec_zero
tozero_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.