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