root_reflectionPerm — Mathlib

English

Another formulation: applying root to the image of j under reflectionPerm i j gives the reflected root: root(reflectionPerm i j) = reflection(i)(root j).

Русский

Другая формулировка: применение корня к изображению j по reflectionPerm i j даёт отражённый корень: root(reflectionPerm i j) = reflection(i)(root j).

LaTeX

$$$ root(reflectionPerm(i,j)) = reflection(i)(root(j)) $$$

Lean4

@[simp]
theorem root_reflectionPerm (j : ι) : P.root (P.reflectionPerm i j) = (P.reflection i) (P.root j) :=
  (P.reflectionPerm_root i j).symm

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