equal
deleted
inserted
replaced
821 lemma mult_inj_if_coprime_nat: |
821 lemma mult_inj_if_coprime_nat: |
822 "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b) |
822 "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b) |
823 \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)" |
823 \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)" |
824 apply(auto simp add:inj_on_def) |
824 apply(auto simp add:inj_on_def) |
825 apply(metis coprime_def dvd_triv_left gcd_proj2_if_dvd_nat gcd_semilattice_nat.inf_commute relprime_dvd_mult) |
825 apply(metis coprime_def dvd_triv_left gcd_proj2_if_dvd_nat gcd_semilattice_nat.inf_commute relprime_dvd_mult) |
826 apply(metis coprime_commute coprime_divprod dvd.neq_le_trans dvd_triv_right) |
826 apply (metis coprime_commute coprime_divprod dvd_triv_right gcd_semilattice_nat.dual_order.strict_trans2) |
827 done |
827 done |
828 |
828 |
829 declare power_Suc0[simp del] |
829 declare power_Suc0[simp del] |
830 |
830 |
831 end |
831 end |