src/HOL/Complex.thy
changeset 56238 5d147e1e18d1
parent 56217 dc429a5b13c4
child 56331 bea2196627cb
equal deleted inserted replaced
56237:69a9dfe71aed 56238:5d147e1e18d1
   396   have "X ----> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
   396   have "X ----> Complex (lim (\<lambda>n. Re (X n))) (lim (\<lambda>n. Im (X n)))"
   397     using tendsto_Complex [OF 1 2] by simp
   397     using tendsto_Complex [OF 1 2] by simp
   398   thus "convergent X"
   398   thus "convergent X"
   399     by (rule convergentI)
   399     by (rule convergentI)
   400 qed
   400 qed
       
   401 
       
   402 declare
       
   403   DERIV_power[where 'a=complex, THEN DERIV_cong,
       
   404               unfolded of_nat_def[symmetric], DERIV_intros]
   401 
   405 
   402 
   406 
   403 subsection {* The Complex Number $i$ *}
   407 subsection {* The Complex Number $i$ *}
   404 
   408 
   405 definition "ii" :: complex  ("\<i>")
   409 definition "ii" :: complex  ("\<i>")