src/HOL/Old_Number_Theory/Primes.thy
changeset 34223 dce32a1e05fe
parent 33657 a4179bf442d1
child 37765 26bdfb7b680b
     1.1 --- a/src/HOL/Old_Number_Theory/Primes.thy	Fri Jan 01 17:21:44 2010 +0100
     1.2 +++ b/src/HOL/Old_Number_Theory/Primes.thy	Fri Jan 01 19:15:43 2010 +0100
     1.3 @@ -820,6 +820,14 @@
     1.4  lemma coprime_divisors: "d dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> coprime d e"
     1.5    by (auto simp add: dvd_def coprime)
     1.6  
     1.7 +lemma mult_inj_if_coprime_nat:
     1.8 +  "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
     1.9 +   \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
    1.10 +apply(auto simp add:inj_on_def)
    1.11 +apply(metis coprime_def dvd_triv_left gcd_proj2_if_dvd_nat gcd_semilattice_nat.inf_commute relprime_dvd_mult)
    1.12 +apply(metis coprime_commute coprime_divprod dvd.neq_le_trans dvd_triv_right)
    1.13 +done
    1.14 +
    1.15  declare power_Suc0[simp del]
    1.16  declare even_dvd[simp del]
    1.17