def
definition
def or abbrev
e_over_phi
show as:
view Lean formalization →
formal statement (Lean)
75noncomputable def e_over_phi : ℝ := exp 1 / phi
e_over_phi
75noncomputable def e_over_phi : ℝ := exp 1 / phi