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

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
hf : StronglySummable f
⊢ StronglyMultipliable f
Tactic:
classical
exact fun d => Finite.subset (finite_toSet _) (support_partialProduct_subset f hf d)
State after:
no goals

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
inst✝ : CommRing α
ι : Type u_3
f : ι → MvPowerSeries σ α
hf : StronglySummable f
⊢ StronglyMultipliable f
Tactic:
exact fun d => Finite.subset (finite_toSet _) (support_partialProduct_subset f hf d)
State after:
no goals