pith. machine review for the scientific record. sign in
lemma proved term proof

partialDeriv_v2_smul

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  69lemma partialDeriv_v2_smul (f : (Fin 4 → ℝ) → ℝ) (c : ℝ) (μ : Fin 4)
  70    (x : Fin 4 → ℝ) (hf : DifferentiableAt ℝ (fun t => f (coordRay x μ t)) 0) :
  71  partialDeriv_v2 (fun y => c * f y) μ x = c * partialDeriv_v2 f μ x := by

proof body

Term-mode proof.

  72  unfold partialDeriv_v2
  73  exact deriv_const_mul c hf
  74
  75/-- Localized version of second derivative linearity (scalar multiplication).
  76    This only requires differentiability in a neighborhood of the point x. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (10)

Lean names referenced from this declaration's body.