# HG changeset patch
# User Alexander Pach <alexander.pach@tum.de>
# Date 1732130580 -3600
#      Wed Nov 20 20:23:00 2024 +0100
# Node ID 4f451ff8ea1da0d0d1eb9b25a1b34457f1596729
# Parent  b8f74d2afb5de069971754d0cfc926acc7486623
adapted to Isabelle/0ed0c4c28903

diff -r b8f74d2afb5d -r 4f451ff8ea1d thys/CRYSTALS-Kyber/Crypto_Scheme.thy
--- a/thys/CRYSTALS-Kyber/Crypto_Scheme.thy	Wed Nov 20 13:52:25 2024 +0000
+++ b/thys/CRYSTALS-Kyber/Crypto_Scheme.thy	Wed Nov 20 20:23:00 2024 +0100
@@ -111,8 +111,8 @@
     by (metis (no_types, lifting) mult.assoc sum.cong sum_distrib_left)
   finally show "(\<Sum>i\<in>UNIV. (\<Sum>j\<in>UNIV. (vec_nth (vec_nth A i) j) * 
     (vec_nth s j)) * (vec_nth r i)) = (\<Sum>j\<in>UNIV. (vec_nth s j) * 
-    (\<Sum>i\<in>UNIV. (vec_nth (vec_nth A i) j) * (vec_nth r i)))" 
-    by blast
+    (\<Sum>i\<in>UNIV. (vec_nth r i) *  (vec_nth (vec_nth A i) j)))"
+    by (simp add: mult.commute)
 qed
 
 text \<open>Lemma about coeff Poly\<close>
diff -r b8f74d2afb5d -r 4f451ff8ea1d thys/Gauss_Jordan/Code_Matrix.thy
--- a/thys/Gauss_Jordan/Code_Matrix.thy	Wed Nov 20 13:52:25 2024 +0000
+++ b/thys/Gauss_Jordan/Code_Matrix.thy	Wed Nov 20 20:23:00 2024 +0100
@@ -41,7 +41,7 @@
   "vec_nth (A *v x) = (%i. (\<Sum>j\<in>UNIV. A $ i $ j * x $ j))" unfolding matrix_vector_mult_def by fastforce
 
 lemma vector_matrix_mult_code [code abstract]:
-  "vec_nth (x v* A) = (%j. (\<Sum>i\<in>UNIV. A $ i $ j * x $ i))" unfolding vector_matrix_mult_def by fastforce
+  "vec_nth (x v* A) = (%j. (\<Sum>i\<in>UNIV. x $ i * A $ i $ j))" unfolding vector_matrix_mult_def by fastforce
 
 definition mat_row
   where "mat_row k i = vec_lambda (%j. if i = j then k else 0)"
diff -r b8f74d2afb5d -r 4f451ff8ea1d thys/Gauss_Jordan/Matrix_To_IArray.thy
--- a/thys/Gauss_Jordan/Matrix_To_IArray.thy	Wed Nov 20 13:52:25 2024 +0000
+++ b/thys/Gauss_Jordan/Matrix_To_IArray.thy	Wed Nov 20 20:23:00 2024 +0100
@@ -171,7 +171,7 @@
   where "A *iv x = IArray.of_fun (\<lambda>i. sum (\<lambda>j. ((A!!i)!!j) * (x!!j)) {0..<IArray.length x}) (nrows_iarray A)"
 
 definition vector_matrix_mult_iarray :: "'a::{semiring_1} iarray => 'a iarray iarray => 'a iarray" (infixl \<open>v*i\<close> 70)
-  where "x v*i A = IArray.of_fun (\<lambda>j. sum (\<lambda>i. ((A!!i)!!j) * (x!!i)) {0..<IArray.length x}) (ncols_iarray A)"
+  where "x v*i A = IArray.of_fun (\<lambda>j. sum (\<lambda>i. (x!!i) * ((A!!i)!!j)) {0..<IArray.length x}) (ncols_iarray A)"
 
 definition mat_iarray :: "'a::{zero} => nat => 'a iarray iarray"
   where "mat_iarray k n = tabulate2 n n (\<lambda> i j. if i = j then k else 0)"
@@ -336,7 +336,7 @@
 proof (auto)
   fix xa
   have "(UNIV::'n set) = from_nat `{0..<CARD('n)}"  using bij_from_nat[where ?'a='n] unfolding bij_betw_def by fast
-  show "(\<Sum>i\<in>UNIV. A $ i $ from_nat xa * x $ i) = (\<Sum>i = 0..<CARD('n). A $ from_nat i $ from_nat xa * x $ from_nat i)"
+  show "(\<Sum>i\<in>UNIV. x $ i * A $ i $ from_nat xa) = (\<Sum>i = 0..<CARD('n). x$ from_nat i * A $ from_nat i $ from_nat xa)"
   using sum.reindex[of "from_nat::nat=>'n"]  using bij_from_nat[where ?'a='n] unfolding bij_betw_def by force
 qed
 
diff -r b8f74d2afb5d -r 4f451ff8ea1d thys/QR_Decomposition/Matrix_To_IArray_QR.thy
--- a/thys/QR_Decomposition/Matrix_To_IArray_QR.thy	Wed Nov 20 13:52:25 2024 +0000
+++ b/thys/QR_Decomposition/Matrix_To_IArray_QR.thy	Wed Nov 20 20:23:00 2024 +0100
@@ -180,7 +180,7 @@
   where "A *iv x = IArray.of_fun (\<lambda>i. sum (\<lambda>j. ((A!!i)!!j) * (x!!j)) {0..<IArray.length x}) (nrows_iarray A)"
 
 definition vector_matrix_mult_iarray :: "'a::{semiring_1} iarray => 'a iarray iarray => 'a iarray" (infixl \<open>v*i\<close> 70)
-  where "x v*i A = IArray.of_fun (\<lambda>j. sum (\<lambda>i. ((A!!i)!!j) * (x!!i)) {0..<IArray.length x}) (ncols_iarray A)"
+  where "x v*i A = IArray.of_fun (\<lambda>j. sum (\<lambda>i. (x!!i) * ((A!!i)!!j)) {0..<IArray.length x}) (ncols_iarray A)"
 
 definition mat_iarray :: "'a::{zero} => nat => 'a iarray iarray"
   where "mat_iarray k n = tabulate2 n n (\<lambda> i j. if i = j then k else 0)"
@@ -344,7 +344,7 @@
   unfolding o_def tabulate2_def nrows_iarray_def ncols_iarray_def matrix_to_iarray_def vec_to_iarray_def
 proof (auto)
   fix xa
-  show "(\<Sum>i\<in>UNIV. A $ i $ from_nat xa * x $ i) = (\<Sum>i = 0..<CARD('n). A $ from_nat i $ from_nat xa * x $ from_nat i)"
+  show "(\<Sum>i\<in>UNIV. x $ i * A $ i $ from_nat xa) = (\<Sum>i = 0..<CARD('n). x $ from_nat i * A $ from_nat i $ from_nat xa)"
     apply (rule sum.reindex_cong[of "from_nat::nat=>'n"]) using bij_from_nat[where ?'a='n] unfolding bij_betw_def by fast+
 qed
 
diff -r b8f74d2afb5d -r 4f451ff8ea1d thys/Rank_Nullity_Theorem/Fundamental_Subspaces.thy
--- a/thys/Rank_Nullity_Theorem/Fundamental_Subspaces.thy	Wed Nov 20 13:52:25 2024 +0000
+++ b/thys/Rank_Nullity_Theorem/Fundamental_Subspaces.thy	Wed Nov 20 20:23:00 2024 +0100
@@ -30,10 +30,12 @@
 
 subsubsection\<open>Relationships among them\<close>
 
-lemma left_null_space_eq_null_space_transpose: "left_null_space A = null_space (transpose A)"
+lemma left_null_space_eq_null_space_transpose:
+  "left_null_space (A::'a::{comm_semiring_1}^'n^'m) = null_space (transpose A)"
   unfolding null_space_def left_null_space_def transpose_vector ..
 
-lemma null_space_eq_left_null_space_transpose: "null_space A = left_null_space (transpose A)" 
+lemma null_space_eq_left_null_space_transpose:
+  "null_space (A::'a::{comm_semiring_1}^'n^'m) = left_null_space (transpose A)"
   using left_null_space_eq_null_space_transpose[of "transpose A"]
   unfolding transpose_transpose ..
 
diff -r b8f74d2afb5d -r 4f451ff8ea1d thys/Rank_Nullity_Theorem/Miscellaneous.thy
--- a/thys/Rank_Nullity_Theorem/Miscellaneous.thy	Wed Nov 20 13:52:25 2024 +0000
+++ b/thys/Rank_Nullity_Theorem/Miscellaneous.thy	Wed Nov 20 20:23:00 2024 +0100
@@ -54,7 +54,7 @@
 lemma finite_columns: "finite (columns A)"
   using finite_Atleast_Atmost_nat[of "\<lambda>i. column i A"] unfolding columns_def .
 
-lemma transpose_vector: "x v* A = transpose A *v x"
+lemma transpose_vector: "x v* A = transpose A *v (x::'a::comm_semiring_1^'m)"
   by simp
 
 lemma transpose_zero[simp]: "(transpose A = 0) = (A = 0)"
@@ -73,7 +73,8 @@
   shows "x v* (k *k A) = k *s (x v* A)"
   using scalar_vector_matrix_assoc 
   unfolding vector_matrix_mult_def matrix_scalar_mult_def vec_eq_iff
-  by (auto simp add: sum_distrib_left vector_space_over_itself.scale_scale)
+  by (simp add: sum_distrib_left vector_space_over_itself.scale_scale) 
+   (simp add: mult.commute)
 
 lemma transpose_scalar: "transpose (k *k A) = k *k transpose A"
   unfolding transpose_def