no goals
𝕂 : Type u_2
𝔸 : Type u_1
inst✝⁵ : Field 𝕂
inst✝⁴ : Ring 𝔸
inst✝³ : Algebra 𝕂 𝔸
inst✝² : TopologicalSpace 𝔸
inst✝¹ : TopologicalRing 𝔸
inst✝ : T2Space 𝔸
x : 𝔸ᵐᵒᵖ
⊢ exp 𝕂 (MulOpposite.unop x) = MulOpposite.unop (exp 𝕂 x)
simp_rw [exp, expSeries_sum_eq, ← MulOpposite.unop_pow, ← MulOpposite.unop_smul, tsum_unop]