inductive definition def or abbrev

`SMCharge`

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

formal statement (Lean)

 133inductive SMCharge where
 134  | electric : SMCharge
 135  | baryon : SMCharge
 136  | lepton : SMCharge
 137  deriving DecidableEq, Fintype
 138

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

charge_to_axis in IndisputableMonolith.Foundation.TopologicalConservation decl_use
sm_charge_count in IndisputableMonolith.Foundation.TopologicalConservation decl_use
sm_charges_match_D3 in IndisputableMonolith.Foundation.TopologicalConservation decl_use
topological_conservation_certificate in IndisputableMonolith.Foundation.TopologicalConservation decl_use
all_threes_unified in IndisputableMonolith.Foundation.WindingCharges decl_use
winding_charges_certificate in IndisputableMonolith.Foundation.WindingCharges decl_use