def
definition
def or abbrev
e_2P_eV
show as:
view Lean formalization →
formal statement (Lean)
103def e_2P_eV : ℚ := 34/10 -- 3.4 eV
proof body
Definition body.
104
105/-- Without QED, 2S and 2P are degenerate. -/