def definition def or abbrev

`sectorOf`

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

formal statement (Lean)

  38def sectorOf : Fermion → Sector
  39| .d | .s | .b => .down
  40| .u | .c | .t => .up
  41| .e | .mu | .tau => .lepton
  42| .nu1 | .nu2 | .nu3 => .neutrino
  43

used by (8)

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

QuarkAbsoluteMassResidual in IndisputableMonolith.Masses.QuarkScoreCard decl_use
sectorOf in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
ZOf in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
sectorOf in IndisputableMonolith.Masses.RungConstructor.Basic decl_use
compute_rung in IndisputableMonolith.Masses.RungConstructor.Motif decl_use
compute_rung_sdgt in IndisputableMonolith.Masses.RungConstructor.Motif decl_use
electron_Z_value in IndisputableMonolith.Physics.ElectronMass.Necessity decl_use
ZOf in IndisputableMonolith.RSBridge.Anchor decl_use

depends on (11)

Lean names referenced from this declaration's body.

mu in IndisputableMonolith.Cost.Ndim.Projector decl_use
Sector in IndisputableMonolith.Masses.Anchor decl_use
tau in IndisputableMonolith.Masses.Anchor decl_use
Fermion in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
Sector in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
sectorOf in IndisputableMonolith.Masses.RSBridge.Anchor decl_use
Sector in IndisputableMonolith.Masses.RungConstructor.Basic decl_use
sectorOf in IndisputableMonolith.Masses.RungConstructor.Basic decl_use
Fermion in IndisputableMonolith.Masses.SMVerification decl_use
Fermion in IndisputableMonolith.RSBridge.Anchor decl_use
Sector in IndisputableMonolith.RSBridge.Anchor decl_use