reflectionPerm_self — Mathlib

English

The image of the root set under reflection i is exactly the root set.

Русский

Образ множества корней под действием отражения i равен самому множеству корней.

LaTeX

$$$ P.reflection(i)''(\operatorname{range}(P.root)) = \operatorname{range}(P.root) $$$

Lean4

@[simp]
theorem reflectionPerm_self : P.reflectionPerm i (P.reflectionPerm i j) = j :=
  by
  apply P.root.injective
  simp only [root_reflectionPerm, reflection_same]

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