∀ {σ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (n : σ →₀ ℕ)
  (a : R), (MvPowerSeries.map f) ((MvPowerSeries.monomial n) a) = (MvPowerSeries.monomial n) (f a)