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_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}.

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

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

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

Pullback IsDomain instance along an injective function.