feat(algebra): generalize ring_hom.map_dvd (#8722)

Now it is available for `mul_hom` and `monoid_hom`, and in a `monoid` (or `semiring` in the `ring_hom` case), not just `comm_semiring`

src/algebra/divisibility.lean

@@ -76,6 +76,18 @@ dvd.elim h (λ d h', begin rw [h', mul_assoc], apply dvd_mul_right end)
 theorem dvd_of_mul_right_dvd (h : a * b ∣ c) : a ∣ c :=
 dvd.elim h (begin intros d h₁, rw [h₁, mul_assoc], apply dvd_mul_right end)
 
+section map_dvd
+
+variables {M N : Type*}
+
+lemma mul_hom.map_dvd [monoid M] [monoid N] (f : mul_hom M N) {a b} : a ∣ b → f a ∣ f b
+| ⟨c, h⟩ := ⟨f c, h.symm ▸ f.map_mul a c⟩
+
+lemma monoid_hom.map_dvd [monoid M] [monoid N] (f : M →* N) {a b} : a ∣ b → f a ∣ f b :=
+f.to_mul_hom.map_dvd
+
+end map_dvd
+
 end monoid
 
 section comm_monoid

src/algebra/ring/basic.lean

@@ -529,6 +529,9 @@ variables [semiring α] {a : α}
 
 @[simp] theorem two_dvd_bit0 : 2 ∣ bit0 a := ⟨a, bit0_eq_two_mul _⟩
 
+lemma ring_hom.map_dvd [semiring β] (f : α →+* β) {a b : α} : a ∣ b → f a ∣ f b :=
+f.to_monoid_hom.map_dvd
+
 end semiring
 
 /-- A commutative semiring is a `semiring` with commutative multiplication. In other words, it is a
@@ -566,9 +569,6 @@ protected def function.surjective.comm_semiring [has_zero γ] [has_one γ] [has_
 lemma add_mul_self_eq (a b : α) : (a + b) * (a + b) = a*a + 2*a*b + b*b :=
 by simp only [two_mul, add_mul, mul_add, add_assoc, mul_comm b]
 
-lemma ring_hom.map_dvd (f : α →+* β) {a b : α} : a ∣ b → f a ∣ f b :=
-λ ⟨z, hz⟩, ⟨f z, by rw [hz, f.map_mul]⟩
-
 end comm_semiring
 
 /-!