def
definition
def or abbrev
higgsFermionCoupling
show as:
view Lean formalization →
formal statement (Lean)
235noncomputable def higgsFermionCoupling (m_f v : ℝ) : ℝ := m_f / v