pairingIn_mul_eq_pairingIn_mul_swap

English

For all i,j, the coxeterWeightIn S i j is nonnegative, reflecting nonnegativity properties of the root system with respect to the root-positive form.

Русский

Для всех i,j коэффициент CoxeterWeightIn S i j неотрицателен, что отражает неотрицательность в корневой системе относительно корневой положительной формы.

LaTeX

$$$ 0 \\le P.coxeterWeightIn S i j $$$

Lean4

theorem pairingIn_mul_eq_pairingIn_mul_swap : P.pairingIn S j i * B.rootLength i = P.pairingIn S i j * B.rootLength j :=
  by
  simpa only [← (algebraMap_injective S R).eq_iff, algebraMap_pairingIn, map_mul, B.algebraMap_rootLength] using
    B.toInvariantForm.pairing_mul_eq_pairing_mul_swap i j

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