equal
deleted
inserted
replaced
315 by (simp add: Suc_times_binomial_eq del: mult_Suc mult_Suc_right) |
315 by (simp add: Suc_times_binomial_eq del: mult_Suc mult_Suc_right) |
316 |
316 |
317 text \<open>Another version of absorption, with \<open>-1\<close> instead of \<open>Suc\<close>.\<close> |
317 text \<open>Another version of absorption, with \<open>-1\<close> instead of \<open>Suc\<close>.\<close> |
318 lemma times_binomial_minus1_eq: "0 < k \<Longrightarrow> k * (n choose k) = n * ((n - 1) choose (k - 1))" |
318 lemma times_binomial_minus1_eq: "0 < k \<Longrightarrow> k * (n choose k) = n * ((n - 1) choose (k - 1))" |
319 using Suc_times_binomial_eq [where n = "n - 1" and k = "k - 1"] |
319 using Suc_times_binomial_eq [where n = "n - 1" and k = "k - 1"] |
320 by (auto split add: nat_diff_split) |
320 by (auto split: nat_diff_split) |
321 |
321 |
322 |
322 |
323 subsection \<open>The binomial theorem (courtesy of Tobias Nipkow):\<close> |
323 subsection \<open>The binomial theorem (courtesy of Tobias Nipkow):\<close> |
324 |
324 |
325 text \<open>Avigad's version, generalized to any commutative ring\<close> |
325 text \<open>Avigad's version, generalized to any commutative ring\<close> |