equal
deleted
inserted
replaced
281 then show "h = g" by (simp add: ext) |
281 then show "h = g" by (simp add: ext) |
282 qed |
282 qed |
283 |
283 |
284 text \<open>TODO: The following lemmas about adjoints should hold for any |
284 text \<open>TODO: The following lemmas about adjoints should hold for any |
285 Hilbert space (i.e. complete inner product space). |
285 Hilbert space (i.e. complete inner product space). |
286 (see \<^url>\<open>http://en.wikipedia.org/wiki/Hermitian_adjoint\<close>) |
286 (see \<^url>\<open>https://en.wikipedia.org/wiki/Hermitian_adjoint\<close>) |
287 \<close> |
287 \<close> |
288 |
288 |
289 lemma adjoint_works: |
289 lemma adjoint_works: |
290 fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space" |
290 fixes f :: "'n::euclidean_space \<Rightarrow> 'm::euclidean_space" |
291 assumes lf: "linear f" |
291 assumes lf: "linear f" |