Theorem: MvPowerSeries.StronglyMultipliable.prod_eq_sum_add_sum (DividedPowers/ForMathlib/MvPowerSeries/StronglySummable/Basic.lean)

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
hf : StronglyMultipliable f
s : Set ι
⊢ hf.prod = ⋯.sum + ⋯.sum
Tactic:
rw [hf.prod_eq, ← hf.add_compl]
State after:
no goals