def
definition
def or abbrev
solar_mass_energy
show as:
view Lean formalization →
formal statement (Lean)
17noncomputable def solar_mass_energy : ℝ := 1.8e54