def
definition
def or abbrev
deltaVar
show as:
view Lean formalization →
formal statement (Lean)
60@[simp] noncomputable def deltaVar (x : ℝ) : ℝ := x
proof body
Definition body.
61
62/-- Functional derivative: δS/δx for action functional S and state variable x. -/