src/HOL/Computational_Algebra/Squarefree.thy
 changeset 67051 e7e54a0b9197 parent 66276 acc3b7dd0b21 child 67399 eab6ce8368fa
```     1.1 --- a/src/HOL/Computational_Algebra/Squarefree.thy	Sat Nov 11 18:33:35 2017 +0000
1.2 +++ b/src/HOL/Computational_Algebra/Squarefree.thy	Sat Nov 11 18:41:08 2017 +0000
1.3 @@ -116,13 +116,16 @@
1.4    show ?thesis unfolding squarefree_factorial_semiring'[OF nz]
1.5    proof
1.6      fix p assume p: "p \<in> prime_factors (a * b)"
1.7 -    {
1.8 +    with nz have "prime p"
1.9 +      by (simp add: prime_factors_dvd)
1.10 +    have "\<not> (p dvd a \<and> p dvd b)"
1.11 +    proof
1.12        assume "p dvd a \<and> p dvd b"
1.13 -      hence "p dvd gcd a b" by simp
1.14 -      also have "gcd a b = 1" by fact
1.15 -      finally have False using nz using p by (auto simp: prime_factors_dvd)
1.16 -    }
1.17 -    hence "\<not>(p dvd a \<and> p dvd b)" by blast
1.18 +      with \<open>coprime a b\<close> have "is_unit p"
1.19 +        by (auto intro: coprime_common_divisor)
1.20 +      with \<open>prime p\<close> show False
1.21 +        by simp
1.22 +    qed
1.23      moreover from p have "p dvd a \<or> p dvd b" using nz
1.24        by (auto simp: prime_factors_dvd prime_dvd_mult_iff)
1.25      ultimately show "multiplicity p (a * b) = 1" using nz p assms(2,3)
1.26 @@ -138,7 +141,7 @@
1.27    shows   "squarefree (prod f A)"
1.28    using assms
1.29    by (induction A rule: infinite_finite_induct)
1.30 -     (auto intro!: squarefree_mult_coprime prod_coprime')
1.31 +     (auto intro!: squarefree_mult_coprime prod_coprime_right)
1.32
1.33  lemma squarefree_powerD: "m > 0 \<Longrightarrow> squarefree (n ^ m) \<Longrightarrow> squarefree n"
1.34    by (cases m) (auto dest: squarefree_multD)
```