reflectionPerm_symm — Mathlib

English

The action of coreflection on a coroot equals the coroot of the reflected root under the reflection-permutation relation.

Русский

Действие coreflection на корoot равно корoot отражённого корня по отношению к отражению-перестановке.

LaTeX

$$$ P.coroot(P.reflectionPerm(i,j)) = (P.coreflection(i))(P.coroot(j)) $$$

Lean4

@[simp]
theorem reflectionPerm_symm : (P.reflectionPerm i).symm = P.reflectionPerm i :=
  Involutive.symm_eq_self_of_involutive (P.reflectionPerm i) <| P.reflectionPerm_involutive i

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