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)