move lemma div_power into semiring_div context; class ring_div inherits from idom
--- a/src/HOL/Divides.thy Sat Jun 13 17:31:56 2009 -0700
+++ b/src/HOL/Divides.thy Mon Jun 15 17:59:36 2009 -0700
@@ -331,17 +331,16 @@
"(a * c) mod (b * c) = (a mod b) * c"
using mod_mult_mult1 [of c a b] by (simp add: mult_commute)
-end
-
lemma div_power:
- "(y::'a::{semiring_div,no_zero_divisors,power}) dvd x \<Longrightarrow>
- (x div y) ^ n = x ^ n div y ^ n"
+ "y dvd x \<Longrightarrow> (x div y) ^ n = x ^ n div y ^ n"
apply (induct n)
apply simp
apply(simp add: div_mult_div_if_dvd dvd_power_same)
done
-class ring_div = semiring_div + comm_ring_1
+end
+
+class ring_div = semiring_div + idom
begin
text {* Negation respects modular equivalence. *}