
diff -r 1eb12389c499 -r a854ca7ca7d9 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Mar 24 21:24:03 2025 +0000
+++ b/src/HOL/Int.thy	Tue Mar 25 21:19:26 2025 +0000
@@ -1881,6 +1881,15 @@
 lemma power_int_mult: "power_int (x :: 'a) (m * n) = power_int (power_int x m) n"
   by (auto simp: power_int_def zero_le_mult_iff simp flip: power_mult power_inverse nat_mult_distrib)
 
+lemma power_int_power: "(a ^ b :: 'a :: division_ring) powi c = a powi (int b * c)"
+  by (subst power_int_mult) simp
+
+lemma power_int_power': "(a powi b :: 'a :: division_ring) ^ c = a powi (b * int c)"
+  by (simp add: power_int_mult)
+
+lemma power_int_nonneg_exp: "n \<ge> 0 \<Longrightarrow> x powi n = x ^ nat n"
+  by (simp add: power_int_def)
+
 end
 
 context




