PhysLean Documentation

PhysLean.Particles.SuperSymmetry.SU5.Charges.OfFieldLabel

Charges assocated with field labels #

Given a field label F, and a charge x : Charges, we can extract the set of charges associated with that field label. This is done by the function ofFieldLabel, which returns a Finset.

theorem SuperSymmetry.SU5.Charges.ext_ofFieldLabel {𝓩 : Type} [InvolutiveNeg 𝓩] {x y : Charges 𝓩} (h : ∀ (F : FieldLabel), x.ofFieldLabel F = y.ofFieldLabel F) :
x = y

Two charges are equal if they are equal on all field labels.