Theorem: MvPowerSeries.StronglySummable.sum_mul' (DividedPowers/ForMathlib/MvPowerSeries/StronglySummable/Basic.lean)

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_4
inst✝ : Semiring α
f : ι → MvPowerSeries σ α
κ : Type u_3
g : κ → MvPowerSeries σ α
hf : StronglySummable f
hg : StronglySummable g
hh : StronglySummable fun i => f i.1 * g i.2
⊢ hh.sum = hf.sum * hg.sum
Tactic:
rw [← sum_mul]
State after:
no goals