def
definition
def or abbrev
m_d_exp
show as:
view Lean formalization →
formal statement (Lean)
48def m_d_exp : ℝ := 4.70
m_d_exp
48def m_d_exp : ℝ := 4.70