𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
a b : E
L : Filter 𝕜
s : Set 𝕜
x : 𝕜
⊢ HasDerivAtFilter (↑f.linear + fun x => ↑f 0) (↑f.linear 1) x L
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
a b : E
L : Filter 𝕜
s : Set 𝕜
x : 𝕜
⊢ HasDerivAtFilter (↑f) (↑f.linear 1) x L
rw [f.decomp]
no goals
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 →ᵃ[𝕜] E
a b : E
L : Filter 𝕜
s : Set 𝕜
x : 𝕜
⊢ HasDerivAtFilter (↑f.linear + fun x => ↑f 0) (↑f.linear 1) x L
exact f.linear.hasDerivAtFilter.add_const (f 0)