# HG changeset patch # User paulson # 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 "(\i. f (i+n)) has_prod a \ (\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 (\i. f (i + n)) \ convergent_prod f" apply safe using convergent_prod_offset apply blast