twoShortAddLong — Mathlib

English

If P is embedded G2, the short root α and long β yield pairings such that α+β is a root, which enforces certain sign constraints on pairingIn.

Русский

Если P встроено в G2, сумма короткого α и длинного β является корнем и задаёт ограничения знаков pairingIn.

LaTeX

$$$ P.pairingIn ℤ i j \in \{-3,-1,0,1,3\} \text{ under root-sum conditions }$$

Lean4

/-- The index of the root `2α + β` where `α` is the short root and `β` is the long root. -/
def twoShortAddLong : ι :=
  P.reflectionPerm (short P) <| P.reflectionPerm (long P) (short P)

Похожие утверждения