def
definition
def or abbrev
theta13_degrees
show as:
view Lean formalization →
formal statement (Lean)
52noncomputable def theta13_degrees : ℝ := 8.57