--- a/src/HOL/Binomial.thy Mon Jan 29 21:18:11 2024 +0100
+++ b/src/HOL/Binomial.thy Tue Jan 30 16:39:21 2024 +0000
@@ -172,16 +172,14 @@
subsection \<open>The binomial theorem (courtesy of Tobias Nipkow):\<close>
text \<open>Avigad's version, generalized to any commutative ring\<close>
-theorem binomial_ring: "(a + b :: 'a::comm_semiring_1)^n =
- (\<Sum>k\<le>n. (of_nat (n choose k)) * a^k * b^(n-k))"
+theorem (in comm_semiring_1) binomial_ring:
+ "(a + b :: 'a)^n = (\<Sum>k\<le>n. (of_nat (n choose k)) * a^k * b^(n-k))"
proof (induct n)
case 0
then show ?case by simp
next
case (Suc n)
- have decomp: "{0..n+1} = {0} \<union> {n + 1} \<union> {1..n}"
- by auto
- have decomp2: "{0..n} = {0} \<union> {1..n}"
+ have decomp: "{0..n+1} = {0} \<union> {n + 1} \<union> {1..n}" and decomp2: "{0..n} = {0} \<union> {1..n}"
by auto
have "(a + b)^(n+1) = (a + b) * (\<Sum>k\<le>n. of_nat (n choose k) * a^k * b^(n - k))"
using Suc.hyps by simp
@@ -208,6 +206,7 @@
by simp
qed
+
text \<open>Original version for the naturals.\<close>
corollary binomial: "(a + b :: nat)^n = (\<Sum>k\<le>n. (of_nat (n choose k)) * a^k * b^(n - k))"
using binomial_ring [of "int a" "int b" n]