Additional lemmas about homomorphisms of semirings and rings

These lemmas have been banished here to avoid unnecessary imports in Mathlib.Algebra.Hom.Ring.Defs.

They could be moved to more natural homes.

theorem RingHom.codomain_trivial_iff_range_eq_singleton_zero {α : Type u_2} {β : Type u_3} : ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), 0 = 1 ↔ Set.range ↑f = {0}

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

theorem RingHom.isUnit_map {α : Type u_2} {β : Type u_3} [Semiring α] [Semiring β] (f : α →+* β) {a : α} : IsUnit a → IsUnit (↑f a)

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

theorem Function.Injective.isDomain {α : Type u_2} {β : Type u_3} [Ring α] [IsDomain α] [Ring β] (f : β →+* α) (hf : Function.Injective ↑f) : IsDomain β

Pullback IsDomain instance along an injective function.