--- 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]
--- a/src/HOL/Computational_Algebra/Primes.thy Mon Jan 29 21:18:11 2024 +0100
+++ b/src/HOL/Computational_Algebra/Primes.thy Tue Jan 30 16:39:21 2024 +0000
@@ -784,6 +784,20 @@
by (auto simp add: prime_factorization_subset_iff_dvd [symmetric]
prime_factorization_prime prime_factors_fact prime_ge_2_nat)
+lemma dvd_choose_prime:
+ assumes kn: "k < n" and k: "k \<noteq> 0" and n: "n \<noteq> 0" and prime_n: "prime n"
+ shows "n dvd (n choose k)"
+proof -
+ have "n dvd (fact n)" by (simp add: fact_num_eq_if n)
+ moreover have "\<not> n dvd (fact k * fact (n-k))"
+ by (metis prime_dvd_fact_iff prime_dvd_mult_iff assms neq0_conv diff_less linorder_not_less)
+ moreover have "(fact n::nat) = fact k * fact (n-k) * (n choose k)"
+ using binomial_fact_lemma kn by auto
+ ultimately show ?thesis using prime_n
+ by (auto simp add: prime_dvd_mult_iff)
+qed
+
+
(* TODO Legacy names *)
lemmas prime_imp_coprime_nat = prime_imp_coprime[where ?'a = nat]
lemmas prime_imp_coprime_int = prime_imp_coprime[where ?'a = int]
--- a/src/HOL/GCD.thy Mon Jan 29 21:18:11 2024 +0100
+++ b/src/HOL/GCD.thy Tue Jan 30 16:39:21 2024 +0000
@@ -2942,4 +2942,11 @@
in [(\<^const_syntax>\<open>semiring_char\<close>, char_type_tr')] end
\<close>
+
+lemma CHAR_not_1 [simp]: "CHAR('a :: {semiring_1, zero_neq_one}) \<noteq> Suc 0"
+ by (metis One_nat_def of_nat_1 of_nat_CHAR zero_neq_one)
+
+lemma (in idom) CHAR_not_1' [simp]: "CHAR('a) \<noteq> Suc 0"
+ using local.of_nat_CHAR by fastforce
+
end