no goals
𝕂 : Type u_2
𝔸 : Type u_1
inst✝⁷ : Field 𝕂
inst✝⁶ : Ring 𝔸
inst✝⁵ : Algebra 𝕂 𝔸
inst✝⁴ : TopologicalSpace 𝔸
inst✝³ : TopologicalRing 𝔸
inst✝² : T2Space 𝔸
inst✝¹ : StarRing 𝔸
inst✝ : ContinuousStar 𝔸
x : 𝔸
⊢ star (exp 𝕂 x) = exp 𝕂 (star x)
simp_rw [exp_eq_tsum, ← star_pow, ← star_inv_nat_cast_smul, ← tsum_star]