added coprimality lemma
authornoschinl
Wed Jun 19 17:33:51 2013 +0200 (2013-06-19)
changeset 52397e95f6b4b1bcf
parent 52396 432777f2e372
child 52398 656e5e171f19
added coprimality lemma
src/HOL/GCD.thy
     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'"