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    }
```