English
For crystallographic, reduced, irreducible P, IsG2 holds exactly when there are indices i,j with pairingInℤ i j = −3.
Русский
Для кристаллизационного, редуцированного, неразложимого P IsG2 выполняется тогда и только тогда, когда существуют i, j такие, что pairingInℤ i j = −3.
LaTeX
$$$ P.IsG2 \iff \exists i,j, P.pairingIn\mathbb{Z} i j = -3 $$$
Lean4
/-- By making an arbitrary choice of roots pairing to `-3`, we can obtain an embedded `𝔤₂` root
system just from the knowledge that such a pairs exists. -/
def toEmbeddedG2 [P.IsG2] : P.EmbeddedG2
where
long := (IsG2.exists_pairingIn_neg_three (P := P)).choose
short := (IsG2.exists_pairingIn_neg_three (P := P)).choose_spec.choose
pairingIn_long_short := (IsG2.exists_pairingIn_neg_three (P := P)).choose_spec.choose_spec
