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

fermionRung

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)

  46def fermionRung : Fermion → ℤ
  47  | .electron => r_lepton "e"
  48  | .muon => r_lepton "mu"
  49  | .tauon => r_lepton "tau"
  50  | .up => r_up "u"
  51  | .charm => r_up "c"
  52  | .top => r_up "t"
  53  | .down => r_down "d"
  54  | .strange => r_down "s"
  55  | .bottom => r_down "b"
  56

used by (1)

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

depends on (11)

Lean names referenced from this declaration's body.