infinite products iff simprule
authorpaulson <lp15@cam.ac.uk>
Fri, 25 Dec 2020 11:44:18 +0000
changeset 73244 cf14976d4fdb
parent 73243 ea0108cefc86
child 73245 83b114a6545f
infinite products iff simprule
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