∀ (R : Type u_2) {M : Type u_5} {N : Type u_6} [inst : Semiring R] [inst_1 : Mul M] [inst_2 : Mul N] (f : M →ₙ* N),
  MonoidAlgebra.mapDomainNonUnitalRingHom R f =
    { toFun := MonoidAlgebra.mapDomain ⇑f, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }