def definition def or abbrev

`particleCharge`

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

formal statement (Lean)

 160def particleCharge : ParticlePair → ℤ
 161  | .particle => 1
 162  | .antiparticle => -1
 163
 164end ConservationLaw
 165
 166/-! ## Ledger Density and Mass -/
 167
 168/-- Ledger density at a point (abstract). -/

depends on (7)

Lean names referenced from this declaration's body.

Mass in IndisputableMonolith.Constants.RSNativeUnits decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use
point in IndisputableMonolith.Numerics.Interval.Basic decl_use
ConservationLaw in IndisputableMonolith.Physics.ConservationLawsFromRS decl_use
density in IndisputableMonolith.Physics.NeutronStarCrustalRegimesFromRS decl_use
ConservationLaw in IndisputableMonolith.RRF.Foundation.Ledger decl_use
ParticlePair in IndisputableMonolith.RRF.Foundation.Ledger decl_use