src/HOL/GCD.thy
 changeset 34222 e33ee7369ecb parent 34221 3ae38d4b090c child 34223 dce32a1e05fe
1.1 --- a/src/HOL/GCD.thy	Fri Jan 01 16:34:51 2010 +0100
1.2 +++ b/src/HOL/GCD.thy	Fri Jan 01 17:21:44 2010 +0100
1.3 @@ -1684,6 +1684,20 @@
1.4    show ?thesis by(simp add: Gcd_def fold_set gcd_commute_int)
1.5  qed
1.7 +
1.8 +lemma mult_inj_if_coprime_nat:
1.9 +  "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
1.10 +   \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
1.11 +apply(auto simp add:inj_on_def)
1.12 +apply (metis coprime_dvd_mult_nat dvd.eq_iff gcd_lcm_lattice_nat.inf_sup_absorb
1.13 +     gcd_semilattice_nat.inf_le2 lcm_proj2_iff_nat nat_mult_1 prod_gcd_lcm_nat)
1.14 +apply (metis coprime_dvd_mult_nat gcd_proj1_if_dvd_nat
1.15 +       gcd_semilattice_nat.inf_commute lcm_dvd1_nat nat_mult_1
1.16 +       nat_mult_commute prod_gcd_lcm_nat)
1.17 +done
1.18 +
1.19 +text{* Nitpick: *}
1.20 +
1.21  lemma gcd_eq_nitpick_gcd [nitpick_def]: "gcd x y \<equiv> Nitpick.nat_gcd x y"
1.22  apply (rule eq_reflection)
1.23  apply (induct x y rule: nat_gcd.induct)