equal
deleted
inserted
replaced
389 using b |
389 using b |
390 by (auto simp add: algebra_simps inner_setsum_left inner_Basis split: if_split intro!: setsum.cong) |
390 by (auto simp add: algebra_simps inner_setsum_left inner_Basis split: if_split intro!: setsum.cong) |
391 also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> b)))" |
391 also have "\<dots> = (\<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> b)))" |
392 using b by (simp add: setsum.delta) |
392 using b by (simp add: setsum.delta) |
393 also have "\<dots> = f x \<bullet> b" |
393 also have "\<dots> = f x \<bullet> b" |
394 by (subst linear_componentwise[symmetric]) (unfold_locales, rule) |
394 by (metis (mono_tags, lifting) Linear_Algebra.linear_componentwise linear_axioms) |
395 finally show "(\<Sum>j\<in>Basis. \<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j)) *\<^sub>R j) \<bullet> b = f x \<bullet> b" . |
395 finally show "(\<Sum>j\<in>Basis. \<Sum>i\<in>Basis. (x \<bullet> i * (f i \<bullet> j)) *\<^sub>R j) \<bullet> b = f x \<bullet> b" . |
396 qed |
396 qed |
397 |
397 |
398 lemma blinfun_of_matrix_apply: |
398 lemma blinfun_of_matrix_apply: |
399 "blinfun_of_matrix a x = (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. ((x \<bullet> j) * a i j) *\<^sub>R i)" |
399 "blinfun_of_matrix a x = (\<Sum>i\<in>Basis. \<Sum>j\<in>Basis. ((x \<bullet> j) * a i j) *\<^sub>R i)" |