pith. machine review for the scientific record. sign in
def definition def or abbrev

sectorOf

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  24def sectorOf : Species → Sector
  25  | .fermion f =>
  26      match RSBridge.sectorOf f with
  27      | .lepton   => .Lepton
  28      | .neutrino => .Neutrino
  29      | .up       => .UpQuark
  30      | .down     => .DownQuark
  31  | .W | .Z | .H => .Electroweak
  32
  33/-- Charge-index q̃ used as input to the constructor motifs. -/

used by (8)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (20)

Lean names referenced from this declaration's body.