src/HOL/Power.thy

--- a/src/HOL/Power.thy	Wed Jul 08 00:04:15 2015 +0200
+++ b/src/HOL/Power.thy	Wed Jul 08 14:01:34 2015 +0200
@@ -306,6 +306,19 @@
 
 end
 
+context normalization_semidom
+begin
+
+lemma normalize_power:
+  "normalize (a ^ n) = normalize a ^ n"
+  by (induct n) (simp_all add: normalize_mult)
+
+lemma unit_factor_power:
+  "unit_factor (a ^ n) = unit_factor a ^ n"
+  by (induct n) (simp_all add: unit_factor_mult)
+
+end
+
 context division_ring
 begin