equal
deleted
inserted
replaced
1604 from assms have "multiplicity p x < 1" |
1604 from assms have "multiplicity p x < 1" |
1605 by (intro multiplicity_lessI) auto |
1605 by (intro multiplicity_lessI) auto |
1606 thus ?thesis by simp |
1606 thus ?thesis by simp |
1607 qed |
1607 qed |
1608 |
1608 |
|
1609 lemma multiplicity_zero_1 [simp]: "multiplicity 0 x = 0" |
|
1610 by (metis (mono_tags) local.dvd_0_left multiplicity_zero not_dvd_imp_multiplicity_0) |
|
1611 |
1609 lemma inj_on_Prod_primes: |
1612 lemma inj_on_Prod_primes: |
1610 assumes "\<And>P p. P \<in> A \<Longrightarrow> p \<in> P \<Longrightarrow> prime p" |
1613 assumes "\<And>P p. P \<in> A \<Longrightarrow> p \<in> P \<Longrightarrow> prime p" |
1611 assumes "\<And>P. P \<in> A \<Longrightarrow> finite P" |
1614 assumes "\<And>P. P \<in> A \<Longrightarrow> finite P" |
1612 shows "inj_on Prod A" |
1615 shows "inj_on Prod A" |
1613 proof (rule inj_onI) |
1616 proof (rule inj_onI) |