--- a/src/HOL/Analysis/Infinite_Products.thy Thu Dec 24 15:40:57 2020 +0000
+++ b/src/HOL/Analysis/Infinite_Products.thy Fri Dec 25 11:44:18 2020 +0000
@@ -1342,7 +1342,7 @@
shows "(\<lambda>i. f (i+n)) has_prod a \<longleftrightarrow> (\<lambda>i. f i) has_prod a"
by (simp add: assms has_prod_iff_shift)
-lemma convergent_prod_iff_shift:
+lemma convergent_prod_iff_shift [simp]:
shows "convergent_prod (\<lambda>i. f (i + n)) \<longleftrightarrow> convergent_prod f"
apply safe
using convergent_prod_offset apply blast