𝕂 : Type u_2
𝔸 : Type u_1
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : TopologicalRing 𝔸
inst✝ : T2Space 𝔸
x y : 𝔸
h : Commute x y
⊢ Commute x ((fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) y)
𝕂 : Type u_2
𝔸 : Type u_1
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : TopologicalRing 𝔸
inst✝ : T2Space 𝔸
x y : 𝔸
h : Commute x y
⊢ Commute x (exp 𝕂 y)
rw [exp_eq_tsum]
no goals
𝕂 : Type u_2
𝔸 : Type u_1
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : TopologicalRing 𝔸
inst✝ : T2Space 𝔸
x y : 𝔸
h : Commute x y
⊢ Commute x ((fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) y)
exact Commute.tsum_right x fun n => (h.pow_right n).smul_right _