∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (χ₁ χ₂ : MulChar R R') (a : Rˣ),
  (MulChar.equivToUnitHom (χ₁ * χ₂)) a = (MulChar.equivToUnitHom χ₁) a * (MulChar.equivToUnitHom χ₂) a