diff -r f8595f6d39a5 -r 07c35dec9dac src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Sun Sep 17 18:56:35 2023 +0100
+++ b/src/HOL/Complex.thy	Sat Sep 23 18:45:19 2023 +0100
@@ -464,6 +464,10 @@
 lemmas Re_suminf = bounded_linear.suminf[OF bounded_linear_Re]
 lemmas Im_suminf = bounded_linear.suminf[OF bounded_linear_Im]
 
+lemma continuous_on_Complex [continuous_intros]:
+  "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> continuous_on A (\<lambda>x. Complex (f x) (g x))"
+  unfolding Complex_eq by (intro continuous_intros)
+
 lemma tendsto_Complex [tendsto_intros]:
   "(f \<longlongrightarrow> a) F \<Longrightarrow> (g \<longlongrightarrow> b) F \<Longrightarrow> ((\<lambda>x. Complex (f x) (g x)) \<longlongrightarrow> Complex a b) F"
   unfolding Complex_eq by (auto intro!: tendsto_intros)
@@ -872,9 +876,6 @@
 lemma i_not_in_Reals [simp, intro]: "\<i> \<notin> \<real>"
   by (auto simp: complex_is_Real_iff)
 
-lemma powr_power_complex: "z \<noteq> 0 \<or> n \<noteq> 0 \<Longrightarrow> (z powr u :: complex) ^ n = z powr (of_nat n * u)"
-  by (induction n) (auto simp: algebra_simps powr_add)
-  
 lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re (cis a ^ n)"
   by (auto simp add: DeMoivre)