def
definition
def or abbrev
weakIsospin
show as:
view Lean formalization →
formal statement (Lean)
210def weakIsospin : ℚ := 1 / 2
proof body
Definition body.
211
212/-- 2I + 1 = 2 (doublet size for I = 1/2). -/