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