--- a/src/HOL/Analysis/Linear_Algebra.thy Sun Sep 15 17:24:31 2019 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy Mon Sep 16 17:03:13 2019 +0100
@@ -369,6 +369,10 @@
lemma bilinear_radd: "bilinear h \<Longrightarrow> h x (y + z) = h x y + h x z"
by (simp add: bilinear_def linear_iff)
+lemma bilinear_times:
+ fixes c::"'a::real_algebra" shows "bilinear (\<lambda>x y::'a. x*y)"
+ by (auto simp: bilinear_def distrib_left distrib_right intro!: linearI)
+
lemma bilinear_lmul: "bilinear h \<Longrightarrow> h (c *\<^sub>R x) y = c *\<^sub>R h x y"
by (simp add: bilinear_def linear_iff)