def
definition
def or abbrev
logVorticity
show as:
view Lean formalization →
formal statement (Lean)
55@[simp] def logVorticity (S : MediumState) : ℝ := S.center.logVorticity
proof body
Definition body.
56
57/-- Convenience: absolute log-vorticity (magnitude proxy). -/