equal
deleted
inserted
replaced
292 by (simp only: mod_div_equality) |
292 by (simp only: mod_div_equality) |
293 finally show ?thesis . |
293 finally show ?thesis . |
294 qed |
294 qed |
295 |
295 |
296 end |
296 end |
|
297 |
|
298 lemma div_mult_div_if_dvd: "(y::'a::{semiring_div,no_zero_divisors}) dvd x \<Longrightarrow> |
|
299 z dvd w \<Longrightarrow> (x div y) * (w div z) = (x * w) div (y * z)" |
|
300 unfolding dvd_def |
|
301 apply clarify |
|
302 apply (case_tac "y = 0") |
|
303 apply simp |
|
304 apply (case_tac "z = 0") |
|
305 apply simp |
|
306 apply (simp add: algebra_simps) |
|
307 apply (subst mult_assoc [symmetric]) |
|
308 apply (simp add: no_zero_divisors) |
|
309 done |
|
310 |
|
311 |
|
312 lemma div_power: "(y::'a::{semiring_div,no_zero_divisors,recpower}) dvd x \<Longrightarrow> |
|
313 (x div y)^n = x^n div y^n" |
|
314 apply (induct n) |
|
315 apply simp |
|
316 apply(simp add: div_mult_div_if_dvd dvd_power_same) |
|
317 done |
297 |
318 |
298 class ring_div = semiring_div + comm_ring_1 |
319 class ring_div = semiring_div + comm_ring_1 |
299 begin |
320 begin |
300 |
321 |
301 text {* Negation respects modular equivalence. *} |
322 text {* Negation respects modular equivalence. *} |