root_indexEquiv_eq_smul — Mathlib

English

For all i in ι, the image of i under the indexEquiv of an automorphism applied to the root equals the action of the automorphism on the root i via the root rep.

Русский

Для каждого i из ι образ i под indexEquiv автоморфизма, применённого к корню, совпадает с действием автоморфизма на корень i через корневое представление.

LaTeX

$$$\\\\text{root}(P)[g.indexEquiv(i)] = g \\cdot P.root(i).$$$

Lean4

@[simp]
theorem root_indexEquiv_eq_smul (i : ι) (g : P.Aut) : P.root (g.indexEquiv i) = g • P.root i := by
  simpa using (congr_fun g.root_weightMap i).symm

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