def
definition
def or abbrev
secondDeriv
show as:
view Lean formalization →
formal statement (Lean)
49noncomputable def secondDeriv (f : (Fin 4 → ℝ) → ℝ) (μ ν : Fin 4)
50 (x : Fin 4 → ℝ) : ℝ :=
proof body
Definition body.
51 deriv (fun s => partialDeriv_v2 f μ (coordRay x ν s)) 0
52
53/-- Laplacian `∇² = Σ_{i=1}^3 ∂²/∂xᵢ²`. -/