def
definition
def or abbrev
m_c_exp
show as:
view Lean formalization →
formal statement (Lean)
50def m_c_exp : ℝ := 1270
m_c_exp
50def m_c_exp : ℝ := 1270