English
The list allRoots collects all 12 roots of the embedded G2, namely longRoot, shortRoot, and all their linear combinations listed in the order shown.
Русский
Список allRoots содержит все 12 корней вложенного g2: длинный корень, короткий корень и все их линейные комбинации в указанном порядке.
LaTeX
$$$\text{allRoots}(P) = [\text{longRoot}(P), -\text{longRoot}(P), \text{shortRoot}(P), -\text{shortRoot}(P), \text{shortAddLongRoot}(P), -\text{shortAddLongRoot}(P), \text{twoShortAddLongRoot}(P), -\text{twoShortAddLongRoot}(P), \text{threeShortAddLongRoot}(P), -\text{threeShortAddLongRoot}(P), \text{threeShortAddTwoLongRoot}(P), -\text{threeShortAddTwoLongRoot}(P)]$$$
Lean4
/-- The list of all 12 roots belonging to the embedded `𝔤₂`. -/
abbrev allRoots : List M :=
[longRoot P, -longRoot P, shortRoot P, -shortRoot P, shortAddLongRoot P, -shortAddLongRoot P, twoShortAddLongRoot P,
-twoShortAddLongRoot P, threeShortAddLongRoot P, -threeShortAddLongRoot P, threeShortAddTwoLongRoot P,
-threeShortAddTwoLongRoot P]
