∀ {σ : Type u_1} {R : Type u_9} [inst : CommSemiring R] (a : σ → R),
  MvPowerSeries.rescale a =
    { toFun := fun f n => (n.prod fun s m => a s ^ m) * (MvPowerSeries.coeff n) f, map_one' := ⋯, map_mul' := ⋯,
      map_zero' := ⋯, map_add' := ⋯ }