src/HOL/Analysis/Cartesian_Euclidean_Space.thy

 lemma box_vec_eq_empty [simp]:
   shows "cbox (vec a) (vec b) = {} \<longleftrightarrow> cbox a b = {}"
         "box (vec a) (vec b) = {} \<longleftrightarrow> box a b = {}"
   by (auto simp: Basis_vec_def mem_box box_eq_empty inner_axis)
 
-lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero)
-
 lemma norm_axis_1 [simp]: "norm (axis m (1::real)) = 1"
   by (simp add: inner_axis' norm_eq_1)
 
 lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0"
   by vector

 lemma vector_mul_lcancel[simp]: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y"
   by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib)
 
 lemma vector_mul_rcancel[simp]: "a *s x = b *s x \<longleftrightarrow> (a::real) = b \<or> x = 0"
   by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib)
-
-lemma vector_mul_lcancel_imp: "a \<noteq> (0::real) ==>  a *s x = a *s y ==> (x = y)"
-  by (metis vector_mul_lcancel)
-
-lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b"
-  by (metis vector_mul_rcancel)
 
 lemma component_le_norm_cart: "\<bar>x$i\<bar> \<le> norm x"
   apply (simp add: norm_vec_def)
   apply (rule member_le_L2_set, simp_all)
   done

   apply (erule_tac x="i" in allE)
   apply (auto simp add: if_distrib cond_application_beta axis_def
     sum.delta[OF finite] cong del: if_weak_cong)
   done
 
-lemma matrix_vector_mul_component: "((A::real^_^_) *v x)$k = (A$k) \<bullet> x"
+lemma matrix_vector_mul_component: "(A *v x)$k = (A$k) \<bullet> x"
   by (simp add: matrix_vector_mult_def inner_vec_def)
 
 lemma dot_lmul_matrix: "((x::real ^_) v* A) \<bullet> y = x \<bullet> (A *v y)"
   apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def sum_distrib_right sum_distrib_left ac_simps)
   apply (subst sum.swap)

 
 lemma transpose_iff [iff]: "transpose A = transpose B \<longleftrightarrow> A = B"
   by (metis transpose_transpose)
 
 lemma matrix_mult_transpose_dot_column:
-  fixes A :: "real^'n^'n"
   shows "transpose A ** A = (\<chi> i j. (column i A) \<bullet> (column j A))"
   by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def column_def inner_vec_def)
 
 lemma matrix_mult_transpose_dot_row:
-  fixes A :: "real^'n^'n"
   shows "A ** transpose A = (\<chi> i j. (row i A) \<bullet> (row j A))"
   by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def row_def inner_vec_def)
 
 text\<open>Two sometimes fruitful ways of looking at matrix-vector multiplication.\<close>
 

   by (simp add: mat_def matrix_def axis_def)
 
 lemma matrix_scaleR: "(matrix (( *\<^sub>R) r)) = mat r"
   by (simp add: mat_def matrix_def axis_def if_distrib cong: if_cong)
 
-lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::real ^ _))"
-  by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff
-      field_simps sum_distrib_left sum.distrib)
+lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::('a::real_algebra_1) ^ _))"
+  by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff field_simps sum.distrib scaleR_right.sum)
 
 lemma
-  fixes A :: "real^'n^'m"
+  fixes A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
   shows matrix_vector_mult_linear_continuous_at [continuous_intros]: "isCont (( *v) A) z"
     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 vector_matrix_left_distrib [algebra_simps]:

   assumes "invertible A"
   shows "inj (( *v) A)"
   by (metis assms inj_on_inverseI invertible_def matrix_vector_mul_assoc matrix_vector_mul_lid)
 
 lemma scalar_invertible:
-  fixes A :: "real^'m^'n"
+  fixes A :: "('a::real_algebra_1)^'m^'n"
   assumes "k \<noteq> 0" and "invertible A"
   shows "invertible (k *\<^sub>R A)"
 proof -
   obtain A' where "A ** A' = mat 1" and "A' ** A = mat 1"
     using assms unfolding invertible_def by auto

   thus "invertible (k *\<^sub>R A)"
     unfolding invertible_def by auto
 qed
 
 lemma scalar_invertible_iff:
-  fixes A :: "real^'m^'n"
+  fixes A :: "('a::real_algebra_1)^'m^'n"
   assumes "k \<noteq> 0" and "invertible A"
   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"