English
For a reduced irreducible root system, either the integer pairings satisfy a swap-or-2 relation for all i,j or they satisfy a swap-or-3 relation for all i,j, after translating to the integer pairing.
Русский
Для уменьшенной нерелизируемой корневой системы либо все пары целочисленных парирований удовлетворяют замене и двойному коэффициенту, либо все пары удовлетворяют замене и тройному коэффициенту, после переноса в целочисленный паринг.
LaTeX
$$$(\forall i,j,\ P.pairingIn ℤ i j = P.pairingIn ℤ j i \lor P.pairingIn ℤ i j = 2 \cdot P.pairingIn ℤ j i \lor P.pairingIn ℤ j i = 2 \cdot P.pairingIn ℤ i j) \lor (\forall i,j,\ P.pairingIn ℤ i j = P.pairingIn ℤ j i \lor P.pairingIn ℤ i j = 3 \cdot P.pairingIn ℤ j i \lor P.pairingIn ℤ j i = 3 \cdot P.pairingIn ℤ i j)$$$
Lean4
theorem forall_pairingIn_eq_swap_or [P.IsReduced] [P.IsIrreducible] :
(∀ i j,
P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
P.pairingIn ℤ i j = 2 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 2 * P.pairingIn ℤ i j) ∨
(∀ i j,
P.pairingIn ℤ i j = P.pairingIn ℤ j i ∨
P.pairingIn ℤ i j = 3 * P.pairingIn ℤ j i ∨ P.pairingIn ℤ j i = 3 * P.pairingIn ℤ i j) :=
by
simpa only [← P.algebraMap_pairingIn ℤ, eq_intCast, ← Int.cast_mul, Int.cast_inj, ← map_ofNat (algebraMap ℤ R)] using
P.forall_pairing_eq_swap_or
