equal
deleted
inserted
replaced
1563 apply (subst setsum_Un_disjoint [THEN sym]) |
1563 apply (subst setsum_Un_disjoint [THEN sym]) |
1564 apply (erule finite_subset, assumption) |
1564 apply (erule finite_subset, assumption) |
1565 apply (rule finite_subset) |
1565 apply (rule finite_subset) |
1566 prefer 2 |
1566 prefer 2 |
1567 apply assumption |
1567 apply assumption |
1568 apply auto |
1568 apply (auto simp add: sup_absorb2) |
1569 apply (rule setsum_cong) |
|
1570 apply auto |
|
1571 done |
1569 done |
1572 |
1570 |
1573 lemma setsum_right_distrib: |
1571 lemma setsum_right_distrib: |
1574 fixes f :: "'a => ('b::semiring_0)" |
1572 fixes f :: "'a => ('b::semiring_0)" |
1575 shows "r * setsum f A = setsum (%n. r * f n) A" |
1573 shows "r * setsum f A = setsum (%n. r * f n) A" |