def definition def or abbrev

`charge_to_axis`

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

formal statement (Lean)

 146def charge_to_axis : SMCharge → Fin 3
 147  | .electric => ⟨0, by norm_num⟩
 148  | .baryon => ⟨1, by norm_num⟩
 149  | .lepton => ⟨2, by norm_num⟩
 150

used by (4)

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

charge_to_axis_bijective in IndisputableMonolith.Foundation.TopologicalConservation decl_use
charge_to_axis_injective in IndisputableMonolith.Foundation.TopologicalConservation decl_use
charge_to_axis_surjective in IndisputableMonolith.Foundation.TopologicalConservation decl_use
topological_conservation_certificate in IndisputableMonolith.Foundation.TopologicalConservation decl_use

depends on (1)

Lean names referenced from this declaration's body.

SMCharge in IndisputableMonolith.Foundation.TopologicalConservation decl_use