Theorems · Theorem · functional analysis

HasFDerivAt.hasFDerivAt_norm_smul

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : StrongDual ℝ E} {x : E} {t : ℝ},
  t ≠ 0 → HasFDerivAt (fun x => ‖x‖) f x → HasFDerivAt (fun x => ‖x‖) (↑(SignType.sign t) • f) (t • x)

Defined in

Mathlib.Analysis.Calculus.FDeriv.Norm

Cited by

4 results in Mathlib

Foundations

Depth 169 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpace