diff -r 1eb12389c499 -r a854ca7ca7d9 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Mon Mar 24 21:24:03 2025 +0000
+++ b/src/HOL/Complex.thy	Tue Mar 25 21:19:26 2025 +0000
@@ -878,6 +878,12 @@
 lemma cis_divide: "cis a / cis b = cis (a - b)"
   by (simp add: divide_complex_def cis_mult)
 
+lemma cis_power_int: "cis x powi n = cis (of_int n * x)"
+  by (auto simp: power_int_def DeMoivre)  
+
+lemma complex_cnj_power_int [simp]: "cnj (x powi n) = cnj x powi n"
+  by (auto simp: power_int_def)
+
 lemma divide_conv_cnj: "norm z = 1 \<Longrightarrow> x / z = x * cnj z"
   by (metis complex_div_cnj div_by_1 mult_1 of_real_1 power2_eq_square)