def
definition
def or abbrev
sin2_theta12_pred
show as:
view Lean formalization →
formal statement (Lean)
127noncomputable def sin2_theta12_pred : ℝ := solar_weight - solar_radiative_correction