∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommRing R'] {R'' : Type u_3} [inst_2 : CommRing R'']
  {f : R' →+* R''}, Function.Injective ⇑f → ∀ {χ : MulChar R R'}, χ.ringHomComp f = 1 ↔ χ = 1