src/HOL/GCD.thy
changeset 52397 e95f6b4b1bcf
parent 51547 604d73671fa7
child 52729 412c9e0381a1
--- a/src/HOL/GCD.thy	Wed Jun 19 17:16:45 2013 +0200
+++ b/src/HOL/GCD.thy	Wed Jun 19 17:33:51 2013 +0200
@@ -714,6 +714,14 @@
     coprime_mult_int[of d a b]
   by blast
 
+lemma coprime_power_int:
+  assumes "0 < n" shows "coprime (a :: int) (b ^ n) \<longleftrightarrow> coprime a b"
+  using assms
+proof (induct n)
+  case (Suc n) then show ?case
+    by (cases n) (simp_all add: coprime_mul_eq_int)
+qed simp
+
 lemma gcd_coprime_exists_nat:
     assumes nz: "gcd (a::nat) b \<noteq> 0"
     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"