src/HOL/Analysis/Generalised_Binomial_Theorem.thy

--- a/src/HOL/Analysis/Generalised_Binomial_Theorem.thy	Mon Jul 16 15:24:06 2018 +0200
+++ b/src/HOL/Analysis/Generalised_Binomial_Theorem.thy	Mon Jul 16 17:50:07 2018 +0200
@@ -70,7 +70,7 @@
   with a show ?thesis by simp
 qed
 
-lemma gen_binomial_complex:
+theorem gen_binomial_complex:
   fixes z :: complex
   assumes "norm z < 1"
   shows   "(\<lambda>n. (a gchoose n) * z^n) sums (1 + z) powr a"