∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [IsDomain S] {φ : R →+* S},
  Function.Injective ⇑φ → ∀ {f : Polynomial R}, f.IsPrimitive → (IsUnit f ↔ IsUnit (Polynomial.map φ f))