def
definition
def or abbrev
r_bottom
show as:
view Lean formalization →
formal statement (Lean)
28def r_bottom : ℕ := 21
proof body
Definition body.
29
30/-- Reference RS-anchored bottom mass at M_Z (approximate MS-bar value at MZ). -/