def definition def or abbrev

`xHessianMatrix2`

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

formal statement (Lean)

  79noncomputable def xHessianMatrix2 (a b x y : ℝ) : Matrix (Fin 2) (Fin 2) ℝ :=

Definition body.

  80  xHessianMatrix2OfR a b x y (aggregate (vec2 a b) (vec2 x y))
  81

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

det_xHessianMatrix2_formula in IndisputableMonolith.Cost.Ndim.XCoordinates decl_use
det_xHessianMatrix2_ne_zero_of_generic in IndisputableMonolith.Cost.Ndim.XCoordinates decl_use
det_xHessianMatrix2_zero_cost in IndisputableMonolith.Cost.Ndim.XCoordinates decl_use
xHessianMatrix2_eq_general in IndisputableMonolith.Cost.Ndim.XCoordinates decl_use

Lean names referenced from this declaration's body.