diff -r ea0108cefc86 -r cf14976d4fdb src/HOL/Analysis/Infinite_Products.thy
--- 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