PhysLean Documentation

PhysLean.Particles.SuperSymmetry.SU5.Charges.MinimallyAllowsTerm.Basic

Minimally allows terms #

Given a set of charges x : Charges corresponding to charges of the representations present in the theory, and a potential term T : PotentialTerm, we say that x minimally allows T if it allows the term T and no proper subset of x allows T.

A collection of charges x : Charges is said to minimally allow the potential term T if it allows T and no strict subset of it allows T.

Equations
Instances For
    theorem SuperSymmetry.SU5.Charges.eq_allowsTermForm_of_minimallyAllowsTerm {𝓩 : Type} [AddCommGroup 𝓩] [DecidableEq 𝓩] {T : PotentialTerm} {x : Charges 𝓩} (h1 : x.MinimallyAllowsTerm T) :
    ∃ (a : 𝓩) (b : 𝓩) (c : 𝓩), x = allowsTermForm a b c T