feat(data/matrix/basic): transform vec_mul to mul_vec (#7348)

src/data/matrix/basic.lean

@@ -644,6 +644,22 @@ lemma smul_mul_vec_assoc (A : matrix m n α) (b : n → α) (a : α) :
   (a • A).mul_vec b = a • (A.mul_vec b) :=
 by { ext, apply smul_dot_product }
 
+lemma mul_vec_add (A : matrix m n α) (x y : n → α) :
+  A.mul_vec (x + y) = A.mul_vec x + A.mul_vec y :=
+by { ext, apply dot_product_add }
+
+lemma add_mul_vec (A B : matrix m n α) (x : n → α) :
+  (A + B).mul_vec x = A.mul_vec x + B.mul_vec x :=
+by { ext, apply add_dot_product }
+
+lemma vec_mul_add (A B : matrix m n α) (x : m → α) :
+  vec_mul x (A + B) = vec_mul x A + vec_mul x B :=
+by { ext, apply dot_product_add }
+
+lemma add_vec_mul (A : matrix m n α) (x y : m → α) :
+  vec_mul (x + y) A = vec_mul x A + vec_mul y A :=
+by { ext, apply add_dot_product }
+
 variables [decidable_eq m] [decidable_eq n]
 
 /--
@@ -742,6 +758,14 @@ lemma mul_vec_smul_assoc (A : matrix m n α) (b : n → α) (a : α) :
   A.mul_vec (a • b) = a • (A.mul_vec b) :=
 by { ext, apply dot_product_smul }
 
+lemma mul_vec_transpose (A : matrix m n α) (x : m → α) :
+  mul_vec Aᵀ x = vec_mul x A :=
+by { ext, apply dot_product_comm }
+
+lemma vec_mul_transpose (A : matrix m n α) (x : n → α) :
+  vec_mul x Aᵀ = mul_vec A x :=
+by { ext, apply dot_product_comm }
+
 end comm_semiring
 
 section transpose