equal
deleted
inserted
replaced
3785 qed |
3785 qed |
3786 |
3786 |
3787 lemma binomial_Vandermonde: |
3787 lemma binomial_Vandermonde: |
3788 "setsum (\<lambda>k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n" |
3788 "setsum (\<lambda>k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n" |
3789 using gbinomial_Vandermonde[of "(of_nat a)" "of_nat b" n] |
3789 using gbinomial_Vandermonde[of "(of_nat a)" "of_nat b" n] |
3790 apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] |
3790 by (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] |
3791 of_nat_setsum[symmetric] of_nat_add[symmetric]) |
3791 of_nat_setsum[symmetric] of_nat_add[symmetric] of_nat_eq_iff) |
3792 apply blast |
|
3793 done |
|
3794 |
3792 |
3795 lemma binomial_Vandermonde_same: "setsum (\<lambda>k. (n choose k)\<^sup>2) {0..n} = (2 * n) choose n" |
3793 lemma binomial_Vandermonde_same: "setsum (\<lambda>k. (n choose k)\<^sup>2) {0..n} = (2 * n) choose n" |
3796 using binomial_Vandermonde[of n n n, symmetric] |
3794 using binomial_Vandermonde[of n n n, symmetric] |
3797 unfolding mult_2 |
3795 unfolding mult_2 |
3798 apply (simp add: power2_eq_square) |
3796 apply (simp add: power2_eq_square) |