Theorems · Theorem · functional analysis

fderiv_norm_smul

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

Defined in

Mathlib.Analysis.Calculus.FDeriv.Norm

Cited by

2 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace