src/HOL/Analysis/Infinite_Products.thy

 lemma has_prod_one_iff_shift:
   assumes "\<And>i. i < n \<Longrightarrow> f i = 1"
   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
   using convergent_prod_ignore_initial_segment convergent_prod_def by blast