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

consequences

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)

 212def consequences : List String := [

proof body

Definition body.

 213  "Electric charge conservation from U(1)",
 214  "Color charge conservation from SU(3)",
 215  "Weak isospin conservation from SU(2)",
 216  "Photon, gluons, W/Z bosons as gauge fields"
 217]
 218
 219/-! ## The Higgs Mechanism and Symmetry Breaking -/
 220
 221/-- **THEOREM**: After symmetry breaking, W and Z are massive but photon is massless.
 222    This is encoded in the particle mass structure. -/

used by (18)

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

depends on (14)

Lean names referenced from this declaration's body.