Theorem: MvPowerSeries.StronglySummable.multipliable_of_one_add (DividedPowers/ForMathlib/MvPowerSeries/StronglySummable/Topology.lean)

State before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι✝ : Type u_3
f✝ : ι✝ → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
ι : Type u_4
f : ι → MvPowerSeries σ α
hf : StronglySummable f
⊢ Multipliable fun i => 1 + f i
Tactic:
classical exact hf.hasProd_of_one_add.multipliable
State after:
no goals

State before:
σ : Type u_1
α : Type u_2
inst✝³ : DecidableEq σ
ι✝ : Type u_3
f✝ : ι✝ → MvPowerSeries σ α
inst✝² : CommRing α
inst✝¹ : UniformSpace α
inst✝ : UniformAddGroup α
ι : Type u_4
f : ι → MvPowerSeries σ α
hf : StronglySummable f
⊢ Multipliable fun i => 1 + f i
Tactic:
exact hf.hasProd_of_one_add.multipliable
State after:
no goals