no goals
𝕂 : Type u_2
𝔸 : Type u_1
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : TopologicalRing 𝔸
x : 𝔸
n : ℕ
⊢ (↑(expSeries 𝕂 𝔸 n) fun x_1 => x) = (↑n !)⁻¹ • x ^ n
simp [expSeries]