𝕂 : Type u_2
𝔸 : Type u_1
𝔹 : Type ?u.88124
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ HasSum (fun n => ↑(expSeries 𝕂 𝔸 n) fun x_1 => x) (exp 𝕂 x)
𝕂 : Type u_2
𝔸 : Type u_1
𝔹 : Type ?u.88124
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ HasSum (fun n => (↑n !)⁻¹ • x ^ n) (exp 𝕂 x)
rw [← expSeries_apply_eq']
no goals
𝕂 : Type u_2
𝔸 : Type u_1
𝔹 : Type ?u.88124
inst✝⁵ : NontriviallyNormedField 𝕂
inst✝⁴ : NormedRing 𝔸
inst✝³ : NormedRing 𝔹
inst✝² : NormedAlgebra 𝕂 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔹
inst✝ : CompleteSpace 𝔸
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ HasSum (fun n => ↑(expSeries 𝕂 𝔸 n) fun x_1 => x) (exp 𝕂 x)
exact expSeries_hasSum_exp_of_mem_ball x hx