Pulling back rings along injective maps, and pushing them forward along surjective maps

theorem Function.Injective.isDomain {α : Type u_1} {β : Type u_2} [Semiring α] [IsDomain α] [Semiring β] {F : Type u_3} [FunLike F β α] [MonoidWithZeroHomClass F β α] (f : F) (hf : Injective ⇑f) : IsDomain β

Pullback IsDomain instance along an injective function.