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

State before:
σ : Type u_1
α : Type u_2
inst✝² : DecidableEq σ
inst✝¹ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
inst✝ : DecidableEq ι
hf : StronglyMultipliable f
s : Finset ι
⊢ hf.prod = ∏ i ∈ s, (1 + f i) + ⋯.sum
Tactic:
rw [hf.prod_eq_sum_add_sum s, hf.finset_prod_eq s]
State after:
no goals