src/HOL/Analysis/Generalised_Binomial_Theorem.thy
changeset 68643 3db6c9338ec1
parent 66466 aec5d9c88d69
child 70138 bd42cc1e10d0
     1.1 --- a/src/HOL/Analysis/Generalised_Binomial_Theorem.thy	Mon Jul 16 15:24:06 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Generalised_Binomial_Theorem.thy	Mon Jul 16 17:50:07 2018 +0200
     1.3 @@ -70,7 +70,7 @@
     1.4    with a show ?thesis by simp
     1.5  qed
     1.6  
     1.7 -lemma gen_binomial_complex:
     1.8 +theorem gen_binomial_complex:
     1.9    fixes z :: complex
    1.10    assumes "norm z < 1"
    1.11    shows   "(\<lambda>n. (a gchoose n) * z^n) sums (1 + z) powr a"