def
definition
def or abbrev
xHessianMatrix
show as:
view Lean formalization →
formal statement (Lean)
36noncomputable def xHessianMatrix {n : ℕ} (α x : Vec n) : Fin n → Fin n → ℝ :=
proof body
Definition body.
37 fun i j => xHessianEntry α x i j
38