27 "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" |
27 "c * a = c * b \<longleftrightarrow> c = 0 \<or> a = b" |
28 using mult_cancel_right [of a c b] by (simp add: ac_simps) |
28 using mult_cancel_right [of a c b] by (simp add: ac_simps) |
29 |
29 |
30 end |
30 end |
31 |
31 |
32 context semiring_div |
32 context semidom_divide |
33 begin |
33 begin |
34 |
34 |
|
35 lemma div_self [simp]: |
|
36 assumes "a \<noteq> 0" |
|
37 shows "a div a = 1" |
|
38 using assms nonzero_mult_divide_cancel_left [of a 1] by simp |
|
39 |
|
40 lemma dvd_div_mult_self [simp]: |
|
41 "a dvd b \<Longrightarrow> b div a * a = b" |
|
42 by (cases "a = 0") (auto elim: dvdE simp add: ac_simps) |
|
43 |
|
44 lemma dvd_mult_div_cancel [simp]: |
|
45 "a dvd b \<Longrightarrow> a * (b div a) = b" |
|
46 using dvd_div_mult_self [of a b] by (simp add: ac_simps) |
|
47 |
|
48 lemma div_mult_swap: |
|
49 assumes "c dvd b" |
|
50 shows "a * (b div c) = (a * b) div c" |
|
51 proof (cases "c = 0") |
|
52 case True then show ?thesis by simp |
|
53 next |
|
54 case False from assms obtain d where "b = c * d" .. |
|
55 moreover from False have "a * divide (d * c) c = ((a * d) * c) div c" |
|
56 by simp |
|
57 ultimately show ?thesis by (simp add: ac_simps) |
|
58 qed |
|
59 |
|
60 lemma dvd_div_mult: |
|
61 assumes "c dvd b" |
|
62 shows "b div c * a = (b * a) div c" |
|
63 using assms div_mult_swap [of c b a] by (simp add: ac_simps) |
|
64 |
|
65 |
35 text \<open>Units: invertible elements in a ring\<close> |
66 text \<open>Units: invertible elements in a ring\<close> |
36 |
67 |
37 abbreviation is_unit :: "'a \<Rightarrow> bool" |
68 abbreviation is_unit :: "'a \<Rightarrow> bool" |
38 where |
69 where |
39 "is_unit a \<equiv> a dvd 1" |
70 "is_unit a \<equiv> a dvd 1" |