# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1524743748 -3600
# Node ID d345e9c35ae1b9a9da045538319e62dacbeb0a1b
# Parent  d45b78cb86cffec4f3b4e87db3c3f0c520d0401d
some of Jose Divasón's material from Rank_Nullity_Theorem/Miscellaneous

diff -r d45b78cb86cf -r d345e9c35ae1 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Apr 25 21:29:02 2018 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Apr 26 12:55:48 2018 +0100
@@ -1,5 +1,5 @@
 (* Title:      HOL/Analysis/Cartesian_Euclidean_Space.thy
-   Some material by Tim Makarios and L C Paulson
+   Some material by Jose Divasón, Tim Makarios and L C Paulson
 *)
 
 section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space\<close>
@@ -714,7 +714,12 @@
     and matrix_vector_mult_linear_continuous_on [continuous_intros]: "continuous_on S (( *v) A)"
   by (simp_all add: linear_linear linear_continuous_at linear_continuous_on matrix_vector_mul_linear)
 
-lemma matrix_vector_mult_add_distrib [algebra_simps]:
+lemma vector_matrix_left_distrib [algebra_simps]:
+  shows "(x + y) v* A = x v* A + y v* A"
+  unfolding vector_matrix_mult_def
+  by (simp add: algebra_simps sum.distrib vec_eq_iff)
+
+lemma matrix_vector_right_distrib [algebra_simps]:
   "A *v (x + y) = A *v x + A *v y"
   by (vector matrix_vector_mult_def sum.distrib distrib_left)
 
@@ -817,34 +822,44 @@
   unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
   by simp
 
-lemma vector_matrix_mul_rid:
+lemma vector_scalar_commute:
+  fixes A :: "'a::{field}^'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"
+  shows "(k *s x) v* A = k *s (x v* A)"
+  by (metis transpose_matrix_vector vector_scalar_commute)
+ 
+lemma vector_matrix_mult_0 [simp]: "0 v* A = 0"
+  unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
+
+lemma vector_matrix_mult_0_right [simp]: "x v* 0 = 0"
+  unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
+
+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)
 
-lemma scalar_vector_matrix_assoc:
+lemma scaleR_vector_matrix_assoc:
   fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
   shows "(k *\<^sub>R x) v* A = k *\<^sub>R (x v* A)"
   by (metis matrix_vector_mult_scaleR transpose_matrix_vector)
 
-lemma vector_scalar_matrix_ac:
+lemma vector_scaleR_matrix_ac:
   fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
   shows "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
 proof -
   have "x v* (k *\<^sub>R A) = (k *\<^sub>R x) v* A"
     unfolding vector_matrix_mult_def
     by (simp add: algebra_simps)
-  with scalar_vector_matrix_assoc
+  with scaleR_vector_matrix_assoc
   show "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
     by auto
 qed
 
-lemma vector_matrix_left_distrib:
-  fixes x y :: "real^'n" and A :: "real^'m^'n"
-  shows "(x + y) v* A = x v* A + y v* A"
-  unfolding vector_matrix_mult_def
-  by (simp add: algebra_simps sum.distrib vec_eq_iff)
-
 
 subsection\<open>Some bounds on components etc. relative to operator norm\<close>
 
@@ -1189,15 +1204,15 @@
     by (simp add: matrix_transpose_mul [symmetric])
 qed
 
-lemma matrix_scalar_vector_ac:
+lemma matrix_scaleR_vector_ac:
   fixes A :: "real^('m::finite)^'n"
   shows "A *v (k *\<^sub>R v) = k *\<^sub>R A *v v"
-  by (metis matrix_vector_mult_scaleR transpose_scalar vector_scalar_matrix_ac vector_transpose_matrix)
+  by (metis matrix_vector_mult_scaleR transpose_scalar vector_scaleR_matrix_ac vector_transpose_matrix)
 
-lemma scalar_matrix_vector_assoc:
+lemma scaleR_matrix_vector_assoc:
   fixes A :: "real^('m::finite)^'n"
   shows "k *\<^sub>R (A *v v) = k *\<^sub>R A *v v"
-  by (metis matrix_scalar_vector_ac matrix_vector_mult_scaleR)
+  by (metis matrix_scaleR_vector_ac matrix_vector_mult_scaleR)
 
 text \<open>Considering an n-element vector as an n-by-1 or 1-by-n matrix.\<close>