src/HOL/Power.thy
changeset 62366 95c6cf433c91
parent 62347 2230b7047376
child 62481 b5d8e57826df
--- a/src/HOL/Power.thy	Thu Feb 18 17:52:53 2016 +0100
+++ b/src/HOL/Power.thy	Thu Feb 18 17:53:09 2016 +0100
@@ -331,6 +331,10 @@
   shows "(a div b) ^ n = a ^ n div b ^ n"
   using assms by (induct n) (simp_all add: div_mult_div_if_dvd dvd_power_same)
 
+lemma is_unit_power_iff:
+  "is_unit (a ^ n) \<longleftrightarrow> is_unit a \<or> n = 0"
+  by (induct n) (auto simp add: is_unit_mult_iff)
+
 end
 
 context normalization_semidom