𝕜 : Type u_1
E : Type u_2
F : Type ?u.2404405
G : Type ?u.2404408
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
⊢ (∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))) ↔
    ∀ᶠ (a : 𝕜) in 𝓝 0,
      HasSum (fun n => ((fun x x_1 => x + x_1) z₀ a - z₀) ^ n • coeff p n) (f ((fun x x_1 => x + x_1) z₀ a))
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2404405
G : Type ?u.2404408
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
⊢ HasFPowerSeriesAt f p z₀ ↔ ∀ᶠ (z : 𝕜) in 𝓝 z₀, HasSum (fun n => (z - z₀) ^ n • coeff p n) (f z)
rw [← map_add_left_nhds_zero, eventually_map, hasFPowerSeriesAt_iff]
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.2404405
G : Type ?u.2404408
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
⊢ (∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun n => z ^ n • coeff p n) (f (z₀ + z))) ↔
    ∀ᶠ (a : 𝕜) in 𝓝 0,
      HasSum (fun n => ((fun x x_1 => x + x_1) z₀ a - z₀) ^ n • coeff p n) (f ((fun x x_1 => x + x_1) z₀ a))
simp_rw [add_sub_cancel']