src/HOL/Analysis/Infinite_Products.thy
changeset 69565 1daf07b65385
parent 69529 4ab9657b3257
child 70113 c8deb8ba6d05
     1.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Tue Jan 01 13:26:37 2019 +0100
     1.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Tue Jan 01 20:57:54 2019 +0100
     1.3 @@ -58,6 +58,7 @@
     1.4    where "raw_has_prod f M p \<equiv> (\<lambda>n. \<Prod>i\<le>n. f (i+M)) \<longlonglongrightarrow> p \<and> p \<noteq> 0"
     1.5  
     1.6  text\<open>The nonzero and zero cases, as in \emph{Complex Analysis} by Joseph Bak and Donald J.Newman, page 241\<close>
     1.7 +text%important \<open>%whitespace\<close>
     1.8  definition%important
     1.9    has_prod :: "(nat \<Rightarrow> 'a::{t2_space, comm_semiring_1}) \<Rightarrow> 'a \<Rightarrow> bool" (infixr "has'_prod" 80)
    1.10    where "f has_prod p \<equiv> raw_has_prod f 0 p \<or> (\<exists>i q. p = 0 \<and> f i = 0 \<and> raw_has_prod f (Suc i) q)"