equal
deleted
inserted
replaced
7 lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}" |
7 lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}" |
8 by (simp add: subspace_def) |
8 by (simp add: subspace_def) |
9 |
9 |
10 lemma delta_mult_idempotent: |
10 lemma delta_mult_idempotent: |
11 "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)" |
11 "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)" |
12 by (cases "k=a") auto |
12 by simp |
13 |
13 |
14 lemma setsum_UNIV_sum: |
14 lemma setsum_UNIV_sum: |
15 fixes g :: "'a::finite + 'b::finite \<Rightarrow> _" |
15 fixes g :: "'a::finite + 'b::finite \<Rightarrow> _" |
16 shows "(\<Sum>x\<in>UNIV. g x) = (\<Sum>x\<in>UNIV. g (Inl x)) + (\<Sum>x\<in>UNIV. g (Inr x))" |
16 shows "(\<Sum>x\<in>UNIV. g x) = (\<Sum>x\<in>UNIV. g (Inl x)) + (\<Sum>x\<in>UNIV. g (Inr x))" |
17 apply (subst UNIV_Plus_UNIV [symmetric]) |
17 apply (subst UNIV_Plus_UNIV [symmetric]) |
810 from h[unfolded lhseq, rule_format, of x] obtain y :: "real ^'m" |
810 from h[unfolded lhseq, rule_format, of x] obtain y :: "real ^'m" |
811 where y: "setsum (\<lambda>i. (y$i) *s column i A) ?U = x" by blast |
811 where y: "setsum (\<lambda>i. (y$i) *s column i A) ?U = x" by blast |
812 have "x \<in> span (columns A)" |
812 have "x \<in> span (columns A)" |
813 unfolding y[symmetric] |
813 unfolding y[symmetric] |
814 apply (rule span_setsum) |
814 apply (rule span_setsum) |
815 apply clarify |
|
816 unfolding scalar_mult_eq_scaleR |
815 unfolding scalar_mult_eq_scaleR |
817 apply (rule span_mul) |
816 apply (rule span_mul) |
818 apply (rule span_superset) |
817 apply (rule span_superset) |
819 unfolding columns_def |
818 unfolding columns_def |
820 apply blast |
819 apply blast |