diff -r 07c802837a8c src/HOL/Analysis/Cartesian_Space.thy
--- a/src/HOL/Analysis/Cartesian_Space.thy	Fri Nov 08 22:52:29 2024 +0100
+++ b/src/HOL/Analysis/Cartesian_Space.thy	Thu Nov 21 20:41:44 2024 +0100
@@ -353,11 +353,6 @@
   shows "invertible (transpose A)"
   by (meson assms invertible_def matrix_left_right_inverse right_invertible_transpose)
 
-lemma vector_matrix_mul_assoc:
-  fixes v :: "('a::comm_semiring_1)^'n"
-  shows "(v v* M) v* N = v v* (M ** N)"
-  by (metis (no_types, opaque_lifting) matrix_transpose_mul matrix_vector_mul_assoc transpose_matrix_vector)
-
 lemma matrix_scaleR_vector_ac:
   fixes A :: "real^('m::finite)^'n"
   shows "A *v (k *\<^sub>R v) = k *\<^sub>R A *v v"
diff -r 07c802837a8c src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Fri Nov 08 22:52:29 2024 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Nov 21 20:41:44 2024 +0100
@@ -986,7 +986,7 @@
 
 definition\<^marker>\<open>tag important\<close> vector_matrix_mult :: "'a ^ 'm \<Rightarrow> ('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n "
     (infixl \<open>v*\<close> 70)
-  where "v v* m == (\<chi> j. sum (\<lambda>i. ((m$i)$j) * (v$i)) (UNIV :: 'm set)) :: 'a^'n"
+  where "v v* m == (\<chi> j. sum (\<lambda>i.  (v$i) * ((m$i)$j)) (UNIV :: 'm set)) :: 'a^'n"
 
 definition\<^marker>\<open>tag unimportant\<close> "(mat::'a::zero => 'a ^'n^'n) k = (\<chi> i j. if i = j then k else 0)"
 definition\<^marker>\<open>tag unimportant\<close> transpose where
@@ -1031,6 +1031,11 @@
   apply simp
   done
 
+proposition vector_matrix_mul_assoc: "(v v* A) v* B = v v* (A ** B)"
+  by (vector matrix_matrix_mult_def vector_matrix_mult_def
+      sum_distrib_left sum_distrib_right mult.assoc)
+      (subst sum.swap, simp)
+
 proposition scalar_matrix_assoc:
   fixes A :: "('a::real_algebra_1)^'m^'n"
   shows "k *\<^sub>R (A ** B) = (k *\<^sub>R A) ** B"
@@ -1207,21 +1212,25 @@
   shows "invertible (k *\<^sub>R A) \<longleftrightarrow> k \<noteq> 0 \<and> invertible A"
   by (simp add: assms scalar_invertible)
 
-lemma vector_transpose_matrix [simp]: "x v* transpose A = A *v x"
-  unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
-  by simp
+lemma vector_transpose_matrix [simp]: 
+  fixes A :: "'a::{comm_semiring_1}^'m^'n"
+  shows "x v* transpose A = A *v x"
+  unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def mult.commute[of "x $ _"]
+  by vector 
 
-lemma transpose_matrix_vector [simp]: "transpose A *v x = x v* A"
-  unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
-  by simp
+lemma transpose_matrix_vector [simp]: 
+  fixes A :: "'a::{comm_semiring_1}^'m^'n"
+  shows "transpose A *v x = x v* A"
+  unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def mult.commute[of "x $ _"]
+  by vector 
 
 lemma vector_scalar_commute:
-  fixes A :: "'a::{field}^'m^'n"
+  fixes A :: "'a::{comm_semiring_1}^'m^'n"
   shows "A *v (c *s x) = c *s (A *v x)"
   by (simp add: vector_scalar_mult_def matrix_vector_mult_def mult_ac sum_distrib_left)
 
 lemma scalar_vector_matrix_assoc:
-  fixes k :: "'a::{field}" and x :: "'a::{field}^'n" and A :: "'a^'m^'n"
+  fixes k :: "'a::{comm_semiring_1}" and x :: "'a::{comm_semiring_1}^'n" and A :: "'a^'m^'n"
   shows "(k *s x) v* A = k *s (x v* A)"
   by (metis transpose_matrix_vector vector_scalar_commute)
  
@@ -1234,7 +1243,8 @@
 lemma vector_matrix_mul_rid [simp]:
   fixes v :: "('a::semiring_1)^'n"
   shows "v v* mat 1 = v"
-  by (metis matrix_vector_mul_lid transpose_mat vector_transpose_matrix)
+  by (vector vector_matrix_mult_def mat_def)
+   (simp add: if_distrib if_distribR cong del: if_weak_cong)
 
 lemma scaleR_vector_matrix_assoc:
   fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
@@ -1253,4 +1263,6 @@
     by auto
 qed
 
+find_theorems "transpose (?A ** ?B)"
+
 end