--- a/src/HOL/Rings.thy Mon Jan 14 18:33:53 2019 +0000
+++ b/src/HOL/Rings.thy Mon Jan 14 18:35:03 2019 +0000
@@ -10,7 +10,7 @@
section \<open>Rings\<close>
theory Rings
- imports Groups Set
+ imports Groups Set Fun
begin
class semiring = ab_semigroup_add + semigroup_mult +
@@ -733,6 +733,17 @@
"c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> a div c = b div c \<longleftrightarrow> a = b"
by (elim dvdE, cases "c = 0") simp_all
+lemma inj_on_mult:
+ "inj_on ((*) a) A" if "a \<noteq> 0"
+proof (rule inj_onI)
+ fix b c
+ assume "a * b = a * c"
+ then have "a * b div a = a * c div a"
+ by (simp only:)
+ with that show "b = c"
+ by simp
+qed
+
end
class idom_divide = idom + semidom_divide