def
definition
def or abbrev
solar_correction
show as:
view Lean formalization →
formal statement (Lean)
112noncomputable def solar_correction : ℝ := (solar_coefficient : ℝ) * alpha
proof body
Definition body.
113