𝕂 : Type u_4
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
F : Type u_1
inst✝ : RingHomClass F 𝔸 𝔹
f : F
hf : Continuous ↑f
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ ↑f ((fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) x) = (fun x_1 => ∑' (n : ℕ), (↑n !)⁻¹ • x_1 ^ n) (↑f x)
𝕂 : Type u_4
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
F : Type u_1
inst✝ : RingHomClass F 𝔸 𝔹
f : F
hf : Continuous ↑f
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ ↑f (exp 𝕂 x) = exp 𝕂 (↑f x)
rw [exp_eq_tsum, exp_eq_tsum]
𝕂 : Type u_4
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
F : Type u_1
inst✝ : RingHomClass F 𝔸 𝔹
f : F
hf : Continuous ↑f
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ (∑' (b : ℕ), (↑f ∘ fun n => (↑n !)⁻¹ • x ^ n) b) = (fun x_1 => ∑' (n : ℕ), (↑n !)⁻¹ • x_1 ^ n) (↑f x)
𝕂 : Type u_4
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
F : Type u_1
inst✝ : RingHomClass F 𝔸 𝔹
f : F
hf : Continuous ↑f
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ ↑f ((fun x => ∑' (n : ℕ), (↑n !)⁻¹ • x ^ n) x) = (fun x_1 => ∑' (n : ℕ), (↑n !)⁻¹ • x_1 ^ n) (↑f x)
refine' ((expSeries_summable_of_mem_ball' _ hx).hasSum.map f hf).tsum_eq.symm.trans _
𝕂 : Type u_4
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
F : Type u_1
inst✝ : RingHomClass F 𝔸 𝔹
f : F
hf : Continuous ↑f
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ (∑' (b : ℕ), ↑f ((↑b !)⁻¹ • x ^ b)) = ∑' (n : ℕ), (↑n !)⁻¹ • ↑f x ^ n
𝕂 : Type u_4
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
F : Type u_1
inst✝ : RingHomClass F 𝔸 𝔹
f : F
hf : Continuous ↑f
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ (∑' (b : ℕ), (↑f ∘ fun n => (↑n !)⁻¹ • x ^ n) b) = (fun x_1 => ∑' (n : ℕ), (↑n !)⁻¹ • x_1 ^ n) (↑f x)
dsimp only [Function.comp]
no goals
𝕂 : Type u_4
𝔸 : Type u_2
𝔹 : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕂
inst✝⁵ : NormedRing 𝔸
inst✝⁴ : NormedRing 𝔹
inst✝³ : NormedAlgebra 𝕂 𝔸
inst✝² : NormedAlgebra 𝕂 𝔹
inst✝¹ : CompleteSpace 𝔸
F : Type u_1
inst✝ : RingHomClass F 𝔸 𝔹
f : F
hf : Continuous ↑f
x : 𝔸
hx : x ∈ EMetric.ball 0 (FormalMultilinearSeries.radius (expSeries 𝕂 𝔸))
⊢ (∑' (b : ℕ), ↑f ((↑b !)⁻¹ • x ^ b)) = ∑' (n : ℕ), (↑n !)⁻¹ • ↑f x ^ n
simp_rw [one_div, map_inv_nat_cast_smul f 𝕂 𝕂, map_pow]