--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Jul 27 16:35:12 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Mon Jul 27 16:52:57 2015 +0100
@@ -255,7 +255,7 @@
done
lemma linear_cmul: "linear f \<Longrightarrow> f (c *\<^sub>R x) = c *\<^sub>R f x"
- by (simp add: linear_iff)
+ by (rule linear.scaleR)
lemma linear_neg: "linear f \<Longrightarrow> f (- x) = - f x"
using linear_cmul [where c="-1"] by simp
@@ -2692,6 +2692,11 @@
with h(1) show ?thesis by blast
qed
+lemma inj_linear_imp_inv_linear:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space"
+ assumes "linear f" "inj f" shows "linear (inv f)"
+using assms inj_iff left_inverse_linear by blast
+
subsection \<open>Infinity norm\<close>