Theorem: MvPowerSeries.IsTopologicallyNilpotent.mul_left (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 α
inst✝ : LinearTopology α
a b : α
hb : IsTopologicallyNilpotent b
⊢ IsTopologicallyNilpotent (a * b)
Tactic:
rw [mul_comm]
State after:
σ : 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 α
inst✝ : LinearTopology α
a b : α
hb : IsTopologicallyNilpotent b
⊢ IsTopologicallyNilpotent (b * a)

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 α
inst✝ : LinearTopology α
a b : α
hb : IsTopologicallyNilpotent b
⊢ IsTopologicallyNilpotent (b * a)
Tactic:
exact mul_right hb a
State after:
no goals