English
From a crystallographic, reduced RootPairing P and a triple (long,short,h) with pairingInℤ(long,short) = 3, one obtains an embedded G2 root system determined by long and short with that relation.
Русский
Из кристаллического, сокращенного RootPairing P и тройки (длинный, короткий, h) с pairingInℤ(long,short) = 3 получают встроенную корневую систему G2, определяемую длинным и коротким корнями с данной связью.
LaTeX
$$$ \text{EmbeddedG2}_{P} \text{ с длинным/коротким} = \text{функция от pairings with } 3$$$
Lean4
/-- A pair of roots which pair to `+3` are also sufficient to distinguish an embedded `𝔤₂`. -/
@[simps]
def ofPairingInThree [CharZero R] [P.IsCrystallographic] [P.IsReduced] (long short : ι)
(h : P.pairingIn ℤ long short = 3) : P.EmbeddedG2
where
long := P.reflectionPerm long long
short := short
pairingIn_long_short := by simp [h]
