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

State before:
σ : Type u_1
α : Type u_2
inst✝¹ : DecidableEq σ
ι : Type u_3
inst✝ : Semiring α
f g : ι → MvPowerSeries σ α
h : f = g
⊢ StronglySummable f ↔ StronglySummable g
Tactic:
rw [h]
State after:
no goals