--- 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)