src/HOL/Analysis/Linear_Algebra.thy
 changeset 69600 86e8e7347ac0 parent 69597 ff784d5a5bfb child 69619 3f7d8e05e0f2
```     1.1 --- a/src/HOL/Analysis/Linear_Algebra.thy	Sat Jan 05 20:12:02 2019 +0100
1.2 +++ b/src/HOL/Analysis/Linear_Algebra.thy	Sun Jan 06 12:32:01 2019 +0100
1.3 @@ -183,7 +183,9 @@
1.4
1.5  subsection \<open>Bilinear functions\<close>
1.6
1.7 -definition%important "bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
1.8 +definition%important
1.9 +bilinear :: "('a::real_vector \<Rightarrow> 'b::real_vector \<Rightarrow> 'c::real_vector) \<Rightarrow> bool" where
1.10 +"bilinear f \<longleftrightarrow> (\<forall>x. linear (\<lambda>y. f x y)) \<and> (\<forall>y. linear (\<lambda>x. f x y))"
1.11
1.12  lemma bilinear_ladd: "bilinear h \<Longrightarrow> h (x + y) z = h x z + h y z"
1.13    by (simp add: bilinear_def linear_iff)
1.14 @@ -239,7 +241,8 @@
1.15
1.16  subsection \<open>Adjoints\<close>
1.17
1.18 -definition%important "adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
1.19 +definition%important adjoint :: "(('a::real_inner) \<Rightarrow> ('b::real_inner)) \<Rightarrow> 'b \<Rightarrow> 'a" where
1.20 +"adjoint f = (SOME f'. \<forall>x y. f x \<bullet> y = x \<bullet> f' y)"
1.21
1.22  lemma adjoint_unique:
1.23    assumes "\<forall>x y. inner (f x) y = inner x (g y)"
```