# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1608896658 0
# Node ID cf14976d4fdb7a00784bfb7e2bb8cdaf382f2897
# Parent  ea0108cefc86643e5f512a4f47a7f00238639275
infinite products iff simprule

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