weylGroup_apply_root — Mathlib

English

The Weyl group action on a root matches the permutation induced by the Weyl group-to-permutation correspondence.

Русский

Действие Weyl-группы на корень совпадает с перестановкой, получаемой из соответствия Weyl-группы и перестановки.

LaTeX

$$$ g \\cdot root_i = root_{weylGroupToPerm(g)(i)} $$$

Lean4

theorem weylGroup_apply_root (g : P.weylGroup) (i : ι) : g • P.root i = P.root (P.weylGroupToPerm g i) :=
  Hom.root_weightMap_apply _ _ _ _

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