Additional lemmas about homomorphisms of semirings and rings

These lemmas were in Mathlib/Algebra/Hom/Ring/Defs.lean and have now been deprecated.

@[deprecated "Use range_eq_singleton_iff and codomain_trivial_iff_range_trivial" (since := "2025-06-09")]

theorem RingHom.codomain_trivial_iff_range_eq_singleton_zero {α : Type u_1} {β : Type u_2} {x✝ : NonAssocSemiring α} {x✝¹ : NonAssocSemiring β} (f : α →+* β) : 0 = 1 ↔ Set.range ⇑f = {0}

f : α →+* β has a trivial codomain iff its range is {0}.

@[deprecated map_dvd (since := "2025-06-09")]

theorem RingHom.map_dvd {α : Type u_1} {β : Type u_2} [Semiring α] [Semiring β] (f : α →+* β) {a b : α} : a ∣ b → f a ∣ f b