src/HOL/Number_Theory/Euclidean_Algorithm.thy
changeset 59010 ec2b4270a502
parent 59009 348561aa3869
child 59061 67771d267ff2
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Nov 17 14:55:33 2014 +0100
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Nov 17 14:55:34 2014 +0100
     1.3 @@ -7,21 +7,6 @@
     1.4  begin
     1.5  
     1.6  context semiring_div
     1.7 -begin
     1.8 -
     1.9 -lemma dvd_setprod [intro]:
    1.10 -  assumes "finite A" and "x \<in> A"
    1.11 -  shows "f x dvd setprod f A"
    1.12 -proof
    1.13 -  from `finite A` have "setprod f (insert x (A - {x})) = f x * setprod f (A - {x})"
    1.14 -    by (intro setprod.insert) auto
    1.15 -  also from `x \<in> A` have "insert x (A - {x}) = A" by blast
    1.16 -  finally show "setprod f A = f x * setprod f (A - {x})" .
    1.17 -qed
    1.18 -
    1.19 -end
    1.20 -
    1.21 -context semiring_div
    1.22  begin 
    1.23  
    1.24  definition ring_inv :: "'a \<Rightarrow> 'a"
    1.25 @@ -1463,7 +1448,7 @@
    1.26        apply (rule no_zero_divisors)
    1.27        apply blast+
    1.28        done
    1.29 -    moreover from `finite A` have "\<forall>x\<in>A. x dvd \<Prod>A" by (intro ballI dvd_setprod)
    1.30 +    moreover from `finite A` have "\<forall>x\<in>A. x dvd \<Prod>A" by blast
    1.31      ultimately have "\<exists>l. l \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd l)" by blast
    1.32      with Lcm0_iff' have "Lcm A \<noteq> 0" by simp
    1.33    }