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

compute_rung_sdgt

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)

 105def compute_rung_sdgt (s : Species) : ℤ :=

proof body

Definition body.

 106  match s with
 107  | .fermion f =>
 108      let sector := sectorOf (.fermion f)
 109      let gen := (RSBridge.genOf f).val
 110      ell_baseline sector + tau_sdgt sector gen
 111  | .W | .Z | .H =>
 112      ell_baseline .Electroweak
 113
 114end RungConstructor
 115end Masses
 116end IndisputableMonolith

used by (27)

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

depends on (17)

Lean names referenced from this declaration's body.