Theorem: MvPowerSeries.tendsto_pow_zero_of_constantCoeff_zero (DividedPowers/ForMathlib/MvPowerSeries/Topology.lean)

State before:
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
f : MvPowerSeries σ α
hf : (constantCoeff σ α) f = 0
⊢ Filter.Tendsto (fun n => f ^ n) Filter.atTop (nhds 0)
Tactic:
apply tendsto_pow_zero_of_constantCoeff_nilpotent
State after:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
f : MvPowerSeries σ α
hf : (constantCoeff σ α) f = 0
⊢ IsNilpotent ((constantCoeff σ α) f)

State before:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
f : MvPowerSeries σ α
hf : (constantCoeff σ α) f = 0
⊢ IsNilpotent ((constantCoeff σ α) f)
Tactic:
rw [hf]
State after:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
f : MvPowerSeries σ α
hf : (constantCoeff σ α) f = 0
⊢ IsNilpotent 0

State before:
case hf
σ : Type u_2
α : Type u_1
inst✝³ : DecidableEq σ
inst✝² : TopologicalSpace α
inst✝¹ : CommRing α
inst✝ : TopologicalRing α
f : MvPowerSeries σ α
hf : (constantCoeff σ α) f = 0
⊢ IsNilpotent 0
Tactic:
exact IsNilpotent.zero
State after:
no goals