Theorem: MvPowerSeries.IsTopologicallyNilpotent.zero (DividedPowers/ForMathlib/MvPowerSeries/Evaluation.lean)

State before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
R : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : TopologicalRing R
S : Type u_3
inst✝⁴ : CommRing S
inst✝³ : TopologicalSpace S
inst✝² : TopologicalRing S
φ : R →+* S
hφ : Continuous ⇑φ
α : Type u_4
inst✝¹ : CommRing α
inst✝ : TopologicalSpace α
x✝ : ℕ
hi : x✝ ≥ 1
⊢ 0 ^ x✝ = 0
Tactic:
rw [zero_pow (Nat.ne_zero_iff_zero_lt.mpr hi)]
State after:
no goals