𝕂 : Type u_2
𝔸 : Type u_1
𝔹 : Type ?u.75852
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedRing 𝔹
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : NormedAlgebra 𝕂 𝔹
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ Summable (norm ∘ fun n => (↑n !)⁻¹ • x ^ n)
𝕂 : Type u_2
𝔸 : Type u_1
𝔹 : Type ?u.75852
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedRing 𝔹
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : NormedAlgebra 𝕂 𝔹
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ Summable fun n => ‖(↑n !)⁻¹ • x ^ n‖
change Summable (norm ∘ _)
𝕂 : Type u_2
𝔸 : Type u_1
𝔹 : Type ?u.75852
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedRing 𝔹
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : NormedAlgebra 𝕂 𝔹
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ Summable (norm ∘ fun n => ↑(expSeries 𝕂 𝔸 n) fun x_1 => x)
𝕂 : Type u_2
𝔸 : Type u_1
𝔹 : Type ?u.75852
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedRing 𝔹
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : NormedAlgebra 𝕂 𝔹
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ Summable (norm ∘ fun n => (↑n !)⁻¹ • x ^ n)
rw [← expSeries_apply_eq']
no goals
𝕂 : Type u_2
𝔸 : Type u_1
𝔹 : Type ?u.75852
inst✝⁴ : NontriviallyNormedField 𝕂
inst✝³ : NormedRing 𝔸
inst✝² : NormedRing 𝔹
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : NormedAlgebra 𝕂 𝔹
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ Summable (norm ∘ fun n => ↑(expSeries 𝕂 𝔸 n) fun x_1 => x)
exact norm_expSeries_summable_of_mem_ball x hx