def definition def or abbrev

`MetallicApply`

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

formal statement (Lean)

  51noncomputable def MetallicApply {n : ℕ}
  52    (p q lam : ℝ) (hInv : Fin n → Fin n → ℝ) (β : Vec n) : Vec n → Vec n :=

Definition body.

  53  fun v => (p / 2) • v + (Real.sqrt (p ^ 2 + 4 * q) / 2) • FApply lam hInv β v
  54

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

Lean names referenced from this declaration's body.