# HG changeset patch
# User paulson
# Date 1608824457 0
# Node ID ea0108cefc86643e5f512a4f47a7f00238639275
# Parent  a4efee8f88425e68103617a5f44ab1af9b9166f9# Parent  fc6597d50b4fbf32a7f140716ccf6d079d1780b2
merged

diff -r a4efee8f8842 -r ea0108cefc86 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Thu Dec 24 14:24:10 2020 +0100
+++ b/src/HOL/Series.thy	Thu Dec 24 15:40:57 2020 +0000
@@ -627,6 +627,29 @@
 
 end
 
+text \<open>Biconditional versions for constant factors\<close>
+context
+  fixes c :: "'a::real_normed_field"
+begin
+
+lemma summable_cmult_iff [simp]: "summable (\<lambda>n. c * f n) \<longleftrightarrow> c=0 \<or> summable f"
+proof -
+  have "\<lbrakk>summable (\<lambda>n. c * f n); c \<noteq> 0\<rbrakk> \<Longrightarrow> summable f"
+    using summable_mult_D by blast
+  then show ?thesis
+    by (auto simp: summable_mult)
+qed
+
+lemma summable_divide_iff [simp]: "summable (\<lambda>n. f n / c) \<longleftrightarrow> c=0 \<or> summable f"
+proof -
+  have "\<lbrakk>summable (\<lambda>n. f n / c); c \<noteq> 0\<rbrakk> \<Longrightarrow> summable f"
+    by (auto dest: summable_divide [where c = "1/c"])
+  then show ?thesis
+    by (auto simp: summable_divide)
+qed
+
+end
+
 lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1"
 proof -
   have 2: "(\<lambda>n. (1/2::real)^n) sums 2"