Theorem: MvPowerSeries.StronglySummable.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
⊢ StronglySummable fun i => f i.1 * g i.2
Tactic:
classical exact fun d => Finite.subset (finite_toSet _) (support_mul hf hg d)
State after:
no goals

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
⊢ StronglySummable fun i => f i.1 * g i.2
Tactic:
exact fun d => Finite.subset (finite_toSet _) (support_mul hf hg d)
State after:
no goals